Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 1 deletions

diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 98e750dfc..c47f59385 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -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.