- Modification de la déf de minus et pred conformément aux remarques de

  Assia et Benjamin W. de telle sorte qu'ils respectent le critère de
  décroissance structurelle lorsqu'utilisés dans un point-fixe.
- Ajout des noms "standard" des lemmes de Peano et correction d'un nom de
  BinInt.



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

2 files changed, 16 insertions, 2 deletions

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index a3b102055..f5c3260de 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -12,7 +12,7 @@
 <<
 Fixpoint minus (n m:nat) {struct n} : nat :=
   match n, m with
-  | O, _ => 0
+  | O, _ => n
   | S k, O => S k
   | S k, S l => k - l
   end
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 3c3f3a093..348034427 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -127,6 +127,20 @@ Proof.
       rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto. 
 Qed.
 
+(** ** Multiplication and successor *)
+
+Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
+Proof.
+  intros; simpl. rewrite plus_comm. reflexivity.
+Qed.
+
+Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
+Proof.
+  induction n as [| p H]; intro m; simpl.
+  reflexivity.
+  rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
+Qed.
+
 (** * Compatibility with orders *)
 
 Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
@@ -246,4 +260,4 @@ Qed.
 
 Ltac tail_simpl :=
   repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
-    simpl in |- *.
\ No newline at end of file
+    simpl in |- *.