(* 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.
now rewrite IHn.
Qed.

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

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

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

(* TP2 exercice 2 *)

Lemma mult_A: forall m, m*0=0.
induction m; now simpl.
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)).
now rewrite <- IHn.
repeat rewrite <- plus_D.
now rewrite (plus_C m n).
Qed. 

Goal forall n m, (n*m=m*n).
induction n; simpl.
intros; now rewrite mult_A.
intros; rewrite mult_B.
now rewrite IHn.
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.
rewrite (plus_C m).
rewrite plus_D.
apply f_equal.
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.
now rewrite H1.
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.
apply IHn.
exists v1.
simpl in H1.
now injection H1.
exists v2.
simpl in H2.
now injection H2.
Qed.