Modularisation of Znat, a few name changed elsewhere

 For instance inj_plus is now Nat2Z.inj_add

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

1 files changed, 7 insertions, 8 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 19c10f87d..a6988f0af 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1566,20 +1566,19 @@ Qed.
 
 (** ** Results about [of_nat] and [of_succ_nat] *)
 
+Lemma of_nat_succ (n:nat) : of_succ_nat n = of_nat (S n).
+Proof.
+ induction n. trivial. simpl. f_equal. now rewrite IHn.
+Qed.
+
 Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
 Proof.
- induction n. trivial.
- simpl. rewrite pred_succ. rewrite <- IHn.
- destruct n. trivial.
- simpl. now rewrite pred_succ.
+ destruct n. trivial. simpl pred. rewrite pred_succ. apply of_nat_succ.
 Qed.
 
 Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.
 Proof.
- intro H.
- rewrite <- pred_of_succ_nat.
- destruct n. now destruct H.
- simpl. now rewrite pred_succ.
+ rewrite of_nat_succ. destruct n; trivial. now destruct 1.
 Qed.
 
 (** ** Correctness proofs for the square root function *)