diff options
Diffstat (limited to 'theories/ZArith/Zbool.v')
| -rw-r--r-- | theories/ZArith/Zbool.v | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 7da91c44..34114d46 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zbool.v 9245 2006-10-17 12:53:34Z notin $ *) +(* $Id: Zbool.v 10063 2007-08-08 14:21:03Z emakarov $ *) Require Import BinInt. Require Import Zeven. @@ -104,7 +104,7 @@ Qed. Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z. Proof. - unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. + unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. case (x ?= y)%Z; intros; discriminate. Qed. @@ -178,6 +178,18 @@ Proof. intro. apply Zle_ge. apply Zle_bool_imp_le. assumption. Qed. +Lemma Zlt_is_lt_bool : forall n m:Z, (n < m)%Z <-> Zlt_bool n m = true. +Proof. +intros n m; unfold Zlt_bool, Zlt. +destruct (n ?= m)%Z; simpl; split; now intro. +Qed. + +Lemma Zgt_is_gt_bool : forall n m:Z, (n > m)%Z <-> Zgt_bool n m = true. +Proof. +intros n m; unfold Zgt_bool, Zgt. +destruct (n ?= m)%Z; simpl; split; now intro. +Qed. + Lemma Zlt_is_le_bool : forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true. Proof. |