Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 38 insertions, 28 deletions

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 73808f92..511c364b 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -5,9 +6,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*)
+(*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Import BinPos.
 Require Import BinInt.
@@ -49,7 +50,7 @@ Proof.
       [ tauto
 	| intros H3; right; unfold not in |- *; intros H4; elim H3; rewrite (H2 H4);
 	  intros H5; discriminate H5 ].
-Qed. 
+Qed.
 
 Theorem dec_Zne : forall n m:Z, decidable (Zne n m).
 Proof.
@@ -79,7 +80,7 @@ Proof.
   intros x y; unfold decidable, Zge in |- *; elim (x ?= y);
     [ left; discriminate
       | right; unfold not in |- *; intros H; apply H; trivial with arith
-      | left; discriminate ]. 
+      | left; discriminate ].
 Qed.
 
 Theorem dec_Zlt : forall n m:Z, decidable (n < m).
@@ -96,7 +97,7 @@ Proof.
       | unfold Zlt in |- *; intros H; elim H; intros H1;
 	[ auto with arith
 	  | right; elim (Zcompare_Gt_Lt_antisym x y); auto with arith ] ].
-Qed. 
+Qed.
 
 (** * Relating strict and large orders *)
 
@@ -180,7 +181,7 @@ Proof.
   intros x y. split. intro. apply Zgt_lt. assumption.
   intro. apply Zlt_gt. assumption.
 Qed.
- 
+
 (** * Equivalence and order properties *)
 
 (** Reflexivity *)
@@ -188,7 +189,7 @@ Qed.
 Lemma Zle_refl : forall n:Z, n <= n.
 Proof.
   intros n; unfold Zle in |- *; rewrite (Zcompare_refl n); discriminate.
-Qed. 
+Qed.
 
 Lemma Zeq_le : forall n m:Z, n = m -> n <= m.
 Proof.
@@ -201,7 +202,7 @@ Hint Resolve Zle_refl: zarith.
 
 Lemma Zle_antisym : forall n m:Z, n <= m -> m <= n -> n = m.
 Proof.
-  intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]]. 
+  intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]].
   absurd (m > n); [ apply Zle_not_gt | apply Zlt_gt ]; assumption.
   assumption.
   absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption.
@@ -256,6 +257,13 @@ Proof.
       | absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ].
 Qed.
 
+Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+  unfold Zle, Zlt. intros.
+  generalize (Zcompare_Eq_iff_eq n m).
+  destruct (n ?= m); intuition; discriminate.
+Qed.
+
 (** Dichotomy *)
 
 Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n.
@@ -276,8 +284,7 @@ Qed.
 
 Lemma Zlt_trans : forall n m p:Z, n < m -> m < p -> n < p.
 Proof.
-  intros n m p H1 H2; apply Zgt_lt; apply Zgt_trans with (m := m); apply Zlt_gt;
-    assumption.
+  exact Zcompare_Lt_trans.
 Qed.
 
 (** Mixed transitivity *)
@@ -400,13 +407,13 @@ Qed.
 Lemma Zgt_le_succ : forall n m:Z, m > n -> Zsucc n <= m.
 Proof.
   unfold Zgt, Zle in |- *; intros n p H; elim (Zcompare_Gt_not_Lt p n);
-    intros H1 H2; unfold not in |- *; intros H3; unfold not in H1; 
+    intros H1 H2; unfold not in |- *; intros H3; unfold not in H1;
       apply H1;
 	[ assumption
 	  | elim (Zcompare_Gt_Lt_antisym (n + 1) p); intros H4 H5; apply H4; exact H3 ].
 Qed.
 
-Lemma Zlt_gt_succ : forall n m:Z, n <= m -> Zsucc m > n.
+Lemma Zle_gt_succ : forall n m:Z, n <= m -> Zsucc m > n.
 Proof.
   intros n p H; apply Zgt_le_trans with p.
   apply Zgt_succ.
@@ -415,7 +422,7 @@ Qed.
 
 Lemma Zle_lt_succ : forall n m:Z, n <= m -> n < Zsucc m.
 Proof.
-  intros n m H; apply Zgt_lt; apply Zlt_gt_succ; assumption.
+  intros n m H; apply Zgt_lt; apply Zle_gt_succ; assumption.
 Qed.
 
 Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m.
@@ -433,12 +440,17 @@ Proof.
   intros n m H; apply Zgt_succ_le; apply Zlt_gt; assumption.
 Qed.
 
-Lemma Zlt_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.
+Lemma Zle_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.
 Proof.
   intros n m H; apply Zle_gt_trans with (m := Zsucc n);
     [ assumption | apply Zgt_succ ].
 Qed.
 
+Lemma Zlt_succ_r : forall n m, n < Zsucc m <-> n <= m.
+Proof.
+  split; [apply Zlt_succ_le | apply Zle_lt_succ].
+Qed.
+
 (** Weakening order *)
 
 Lemma Zle_succ : forall n:Z, n <= Zsucc n.
@@ -478,9 +490,9 @@ Hint Resolve Zle_le_succ: zarith.
 Lemma Zgt_succ_pred : forall n m:Z, m > Zsucc n -> Zpred m > n.
 Proof.
   unfold Zgt, Zsucc, Zpred in |- *; intros n p H;
-    rewrite <- (fun x y => Zcompare_plus_compat x y 1); 
+    rewrite <- (fun x y => Zcompare_plus_compat x y 1);
       rewrite (Zplus_comm p); rewrite Zplus_assoc;
-	rewrite (fun x => Zplus_comm x n); simpl in |- *; 
+	rewrite (fun x => Zplus_comm x n); simpl in |- *;
 	  assumption.
 Qed.
 
@@ -563,7 +575,7 @@ Proof.
   assert (Hle : m <= n).
   apply Zgt_succ_le; assumption.
   destruct (Zle_lt_or_eq _ _ Hle) as [Hlt| Heq].
-  left; apply Zlt_gt; assumption.  
+  left; apply Zlt_gt; assumption.
   right; assumption.
 Qed.
 
@@ -680,7 +692,7 @@ Proof.
   rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial.
 Qed.
 
-(** ** Multiplication *) 
+(** ** Multiplication *)
 (** Compatibility of multiplication by a positive wrt to order *)
 
 Lemma Zmult_le_compat_r : forall n m p:Z, n <= m -> 0 <= p -> n * p <= m * p.
@@ -777,7 +789,7 @@ Proof.
   intros a b c d H0 H1 H2 H3.
   apply Zge_trans with (a * d).
   apply Zmult_ge_compat_l; trivial.
-  apply Zge_trans with c; trivial. 
+  apply Zge_trans with c; trivial.
   apply Zmult_ge_compat_r; trivial.
 Qed.
 
@@ -965,17 +977,17 @@ Qed.
 
 Lemma Zeq_plus_swap : forall n m p:Z, n + p = m <-> n = m - p.
 Proof.
-  intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry  in |- *. rewrite Zplus_comm. 
+  intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry  in |- *. rewrite Zplus_comm.
   assumption.
-  intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse. 
+  intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse.
   rewrite Zplus_opp_l. apply Zplus_0_r.
 Qed.
 
 Lemma Zlt_minus_simpl_swap : forall n m:Z, 0 < m -> n - m < n.
 Proof.
   intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus;
-    pattern n at 1 in |- *; rewrite <- (Zplus_0_r n); 
-      rewrite (Zplus_comm m n); apply Zplus_lt_compat_l; 
+    pattern n at 1 in |- *; rewrite <- (Zplus_0_r n);
+      rewrite (Zplus_comm m n); apply Zplus_lt_compat_l;
 	assumption.
 Qed.
 
@@ -993,8 +1005,8 @@ Qed.
 
 Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m.
 Proof.
-  intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m); 
-    rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. 
+  intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m);
+    rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H.
 Qed.
 
 Lemma Zmult_lt_compat:
@@ -1012,7 +1024,7 @@ Proof.
   rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith.
 Qed.
 
-Lemma Zmult_lt_compat2: 
+Lemma Zmult_lt_compat2:
   forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
 Proof.
   intros n m p q (H1, H2) (H3, H4).
@@ -1025,5 +1037,3 @@ Qed.
 
 (** For compatibility *)
 Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
-Notation Zle_gt_succ := Zlt_gt_succ (only parsing).
-Notation Zle_succ_gt := Zlt_succ_gt (only parsing).