Modularization of Pnat

 For instance, former Pplus_plus is now Pos2Nat.inj_add.
 As usual, compatibility notation are provided.

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

1 files changed, 18 insertions, 1 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 542582bce..5d8d5274f 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -440,7 +440,7 @@ Fixpoint of_nat (n:nat) : positive :=
    | S x => succ (of_nat x)
  end.
 
-(* Another version that convert [n] into [n+1] *)
+(* Another version that converts [n] into [n+1] *)
 
 Fixpoint of_succ_nat (n:nat) : positive :=
   match n with
@@ -1936,6 +1936,23 @@ Proof.
  rewrite H. apply IHp.
 Qed.
 
+(** ** Results about [of_nat] and [of_succ_nat] *)
+
+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.
+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.
+Qed.
 
 (** ** Correctness proofs for the square root function *)