(* TP2 exercice 1 *)
Goal forall m, 0+m=m.
intros; reflexivity.
Qed.

Goal forall n m, (S n +m=S (n+m)).
simpl; reflexivity.
Qed.

Lemma plus_n_0: forall n, (n+0=n).
induction n.
reflexivity.
simpl.
rewrite IHn; reflexivity.
Qed.

Lemma plus_n_Sm: forall n m, ( n + S m=S (n+m)).
induction n.
reflexivity.
intros m.
simpl.
rewrite IHn; reflexivity.
Qed.

Lemma plus_C: forall n m, (n+m=m+n).
induction n.
simpl.
intros; rewrite plus_n_0; reflexivity.
intros.
rewrite plus_n_Sm.
rewrite <- IHn; reflexivity.
Qed.

Lemma plus_D: forall n m p, (n+m)+p=n+(m+p).
induction n.
reflexivity.
simpl.
intros.
rewrite IHn; reflexivity.
Qed.

(* TP2 exercice 2 *)

Lemma mult_A: forall m, m*0=0.
induction m; try intros; simpl; try reflexivity; assumption.
Qed.

Lemma mult_B: forall n m, n*S m=n+n*m.
induction n; simpl.
reflexivity.
intros.
replace  (n + (m + n * m)) with (m+(n+n*m)).
rewrite <- IHn; reflexivity.
repeat rewrite <- plus_D.
rewrite (plus_C m n); reflexivity.
Qed. 

Goal forall n m, (n*m=m*n).
induction n; simpl.
intros; apply sym_eq; apply mult_A.
intros; rewrite mult_B.
rewrite IHn; reflexivity.
Qed.


Goal forall n m p, (n+m)*p = n*p+m*p.
induction p.
repeat rewrite mult_A.
reflexivity.
repeat rewrite mult_B.
rewrite IHp.
repeat rewrite plus_D.
apply f_equal with (f:= fun x => n+x).
rewrite (plus_C m).
rewrite plus_D.
apply f_equal with (f:= fun x => n*p+x).
apply plus_C.
Qed.

(* TP2 exercice 3 *)

Definition le (n m:nat) := exists p, n+p=m.

Lemma le_refl: forall n, le n n.
unfold le; intros n; exists 0.
rewrite plus_n_0.
reflexivity.
Qed.


Lemma le_trans: forall n m p, le n m -> le m p -> le n p.
intros n m p (v1,H1) (v2,H2).
exists (v1+v2).
rewrite <- plus_D.
rewrite H1; assumption.
Qed.


Lemma le_antisym: forall n m, le n m -> le m n -> n = m.
induction n.
intros m (v1,H1) (v2,H2).
induction m.
reflexivity.
discriminate H2.
induction m.
intros (v1,H1) (v2,H2).
discriminate H1.
intros (v1,H1) (v2,H2).
apply f_equal with (f:= fun x => S x).
apply IHn.
exists v1.
simpl in H1.
injection H1; intros; assumption.
exists v2.
simpl in H2.
injection H2; intros; assumption.
Qed.