In agreement with Laurent Thery, start migration of auxiliary results

present in Ints. For the moment, mainly: 
 - Q parts go in QArith
 - Some of the Zdivide & Zgcd stuff go in Znumtheory

More to come ...



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

2 files changed, 18 insertions, 7 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index d7486bc2bb..a910c89220 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -1226,6 +1226,24 @@ Proof.
   intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
 Qed.
 
+(** Number of digits in a number *)
+
+Fixpoint Psize (p:positive) : nat := 
+  match p with 
+    | xH => 1%nat
+    | xI p => S (Psize p) 
+    | xO p => S (Psize p)
+  end.
+
+Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat.
+Proof.
+  assert (le0 : forall n:nat, (0<=n)%nat) by (induction n; auto).
+  assert (leS : forall n m:nat, (n<=m)%nat -> (S n <= S m)%nat) by (induction 1; auto).
+  induction p; destruct q; simpl; auto; intros; try discriminate.
+  intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
+  intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
+Qed.
+
 
 
 
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index cdb669bf66..04f454df4d 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -577,13 +577,6 @@ Qed.
 
 (** Number of digits in a number *)
 
-Fixpoint Psize (p:positive) : nat := 
-  match p with 
-    | xH => 1%nat
-    | xI p => S (Psize p) 
-    | xO p => S (Psize p)
-  end.
-
 Definition Nsize (n:N) : nat := match n with 
   | N0 => 0%nat
   | Npos p => Psize p