Lemmes dans un sens plus naturel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4881 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 0 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 2356c9cb59..d521a845d5 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -119,12 +119,24 @@ Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
 
 V8Infix "*" mult : nat_scope.
 
+Lemma mult_O_r : (n:nat) (mult n O)=O.
+Proof.
+  NewInduction n; Simpl; Auto.
+Qed.
+
 Lemma mult_n_O : (n:nat) O=(mult n O).
 Proof.
   NewInduction n; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_O : core v62.
 
+Lemma mult_S_r : (n,m:nat) (mult n (S m))=(plus (mult n m) n).
+Proof.
+  Intros; NewInduction n as [|p H]; Simpl; Auto.
+  Rewrite H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S).
+  Pattern 1 3 m; Elim m; Simpl; Auto.
+Qed.
+
 Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
 Proof.
   Intros; NewInduction n as [|p H]; Simpl; Auto.