diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-01 01:49:08 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-01 01:49:08 +0000 |
| commit | aa0fa131bb0c5f8239644faf7a5a3069a337bb2f (patch) | |
| tree | 8faa2278655ec472d0f2c72d931b81a7d31c24ff /theories/NArith/BinPos.v | |
| parent | 14071a88408b2a678c8129aebf90e669eee007ee (diff) | |
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
Diffstat (limited to 'theories/NArith/BinPos.v')
| -rw-r--r-- | theories/NArith/BinPos.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index d7486bc2b..a910c8922 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. + |