- 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

1 files changed, 3 insertions, 1 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 1a925cee6..a0bf8e3f8 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -507,11 +507,13 @@ Proof.
       trivial with arith.
 Qed.
 
-Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
+Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
 Proof.
   intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
 Qed.
 
+Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
+
 Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
 Proof.
   unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;