diff options
Diffstat (limited to 'theories/ZArith/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index a1ec4b35..208e84ae 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -66,10 +66,10 @@ Qed. (** * Relating strict and large orders *) -Notation Zgt_lt := Z.gt_lt (compat "8.6"). -Notation Zlt_gt := Z.lt_gt (compat "8.6"). -Notation Zge_le := Z.ge_le (compat "8.6"). -Notation Zle_ge := Z.le_ge (compat "8.6"). +Notation Zgt_lt := Z.gt_lt (compat "8.7"). +Notation Zlt_gt := Z.lt_gt (compat "8.7"). +Notation Zge_le := Z.ge_le (compat "8.7"). +Notation Zle_ge := Z.le_ge (compat "8.7"). Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). Notation Zge_iff_le := Z.ge_le_iff (only parsing). @@ -123,7 +123,7 @@ Qed. (** Reflexivity *) -Notation Zle_refl := Z.le_refl (compat "8.6"). +Notation Zle_refl := Z.le_refl (compat "8.7"). Notation Zeq_le := Z.eq_le_incl (only parsing). Hint Resolve Z.le_refl: zarith. @@ -143,7 +143,7 @@ Qed. (** Irreflexivity *) -Notation Zlt_irrefl := Z.lt_irrefl (compat "8.6"). +Notation Zlt_irrefl := Z.lt_irrefl (compat "8.7"). Notation Zlt_not_eq := Z.lt_neq (only parsing). Lemma Zgt_irrefl n : ~ n > n. @@ -167,7 +167,7 @@ Notation Zle_or_lt := Z.le_gt_cases (only parsing). (** Transitivity of strict orders *) -Notation Zlt_trans := Z.lt_trans (compat "8.6"). +Notation Zlt_trans := Z.lt_trans (compat "8.7"). Lemma Zgt_trans n m p : n > m -> m > p -> n > p. Proof. @@ -176,8 +176,8 @@ Qed. (** Mixed transitivity *) -Notation Zlt_le_trans := Z.lt_le_trans (compat "8.6"). -Notation Zle_lt_trans := Z.le_lt_trans (compat "8.6"). +Notation Zlt_le_trans := Z.lt_le_trans (compat "8.7"). +Notation Zle_lt_trans := Z.le_lt_trans (compat "8.7"). Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p. Proof. @@ -191,7 +191,7 @@ Qed. (** Transitivity of large orders *) -Notation Zle_trans := Z.le_trans (compat "8.6"). +Notation Zle_trans := Z.le_trans (compat "8.7"). Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p. Proof. @@ -257,8 +257,8 @@ Qed. (** Relating strict and large order using successor or predecessor *) -Notation Zlt_succ_r := Z.lt_succ_r (compat "8.6"). -Notation Zle_succ_l := Z.le_succ_l (compat "8.6"). +Notation Zlt_succ_r := Z.lt_succ_r (compat "8.7"). +Notation Zle_succ_l := Z.le_succ_l (compat "8.7"). Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m. Proof. @@ -336,8 +336,8 @@ Qed. (** Special cases of ordered integers *) -Notation Zlt_0_1 := Z.lt_0_1 (compat "8.6"). -Notation Zle_0_1 := Z.le_0_1 (compat "8.6"). +Notation Zlt_0_1 := Z.lt_0_1 (compat "8.7"). +Notation Zle_0_1 := Z.le_0_1 (compat "8.7"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. |