diff options
author | 2010-10-14 16:09:28 +0000 | |
---|---|---|
committer | 2010-10-14 16:09:28 +0000 | |
commit | f26125cfe2a794ca482f3111512ddfb2dd1f3aea (patch) | |
tree | 8261623b26ea6a38561130d0410fe03a39b89120 /theories/Numbers/NatInt/NZDiv.v | |
parent | 0b6f7bd1c74ccfe2cb2272d01b366af08dc9c741 (diff) |
Numbers : also axiomatize constants 1 and 2.
Initially, I was using notation 1 := (S 0) and so on. But then, when
implementing by NArith or ZArith, some lemmas statements were filled
with Nsucc's and Zsucc's instead of 1 and 2's.
Concerning BigN, things are rather complicated: zero, one, two
aren't inlined during the functor application creating BigN.
This is deliberate, at least for the other operations like BigN.add.
And anyway, since zero, one, two are defined too early in NMake,
we don't have 0%bigN in the body of BigN.zero but something complex that
reduce to 0%bigN, same for one and two. Fortunately, apply or
rewrite of generic lemmas seem to work, even if there's BigZ.zero
on one side and 0 on the other...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13555 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt/NZDiv.v')
-rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 3b9720f32..fe66d88c6 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -160,12 +160,12 @@ Qed. Lemma div_1_l: forall a, 1<a -> 1/a == 0. Proof. -intros; apply div_small; split; auto. apply le_succ_diag_r. +intros; apply div_small; split; auto. apply le_0_1. Qed. Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1. Proof. -intros; apply mod_small; split; auto. apply le_succ_diag_r. +intros; apply mod_small; split; auto. apply le_0_1. Qed. Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a. |