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

1 files changed, 17 insertions, 3 deletions

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 93201964e..e2e398025 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -231,19 +231,33 @@ Qed.
 
 Theorem lt_0_1 : 0 < 1.
 Proof.
-apply lt_succ_diag_r.
+rewrite one_succ. apply lt_succ_diag_r.
 Qed.
 
 Theorem le_0_1 : 0 <= 1.
 Proof.
-apply le_succ_diag_r.
+apply lt_le_incl, lt_0_1.
+Qed.
+
+Theorem lt_0_2 : 0 < 2.
+Proof.
+transitivity 1. apply lt_0_1. rewrite two_succ. apply lt_succ_diag_r.
+Qed.
+
+Theorem le_0_2 : 0 <= 2.
+Proof.
+apply lt_le_incl, lt_0_2.
 Qed.
 
 Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
 Proof.
-intros n m H1 H2. apply <- le_succ_l in H1. order.
+intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order.
 Qed.
 
+(** The order tactic enriched with some knowledge of 0,1,2 *)
+
+Ltac order' := generalize lt_0_1 lt_0_2; order.
+
 
 (** More Trichotomy, decidability and double negation elimination. *)