From d7a3d9b4fbfdd0df8ab4d0475fc7afa1ed5f5bcb Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 14 Oct 2010 11:37:26 +0000
Subject: Zeven: some complements, e.g. proofs that Zeven_bool and co are ok

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13545 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zeven.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 05716af5f8..74e2e6fbf6 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -49,6 +49,16 @@ Definition Zodd_bool (z:Z) :=
     | _ => true
   end.
 
+Lemma Zeven_bool_iff : forall n, Zeven_bool n = true <-> Zeven n.
+Proof.
+ destruct n as [|p|p]; try destruct p; simpl in *; split; easy.
+Qed.
+
+Lemma Zodd_bool_iff : forall n, Zodd_bool n = true <-> Zodd n.
+Proof.
+ destruct n as [|p|p]; try destruct p; simpl in *; split; easy.
+Qed.
+
 Definition Zeven_odd_dec : forall z:Z, {Zeven z} + {Zodd z}.
 Proof.
   intro z. case z;
@@ -237,6 +247,16 @@ Proof.
   destruct p; simpl; auto.
 Qed.
 
+Theorem Zeven_ex_iff : forall n, Zeven n <-> exists m, n = 2*m.
+Proof.
+ split. apply Zeven_ex. intros (m,->). apply Zeven_2p.
+Qed.
+
+Theorem Zodd_ex_iff : forall n, Zodd n <-> exists m, n = 2*m + 1.
+Proof.
+ split. apply Zodd_ex. intros (m,->). apply Zodd_2p_plus_1.
+Qed.
+
 Theorem Zeven_plus_Zodd: forall a b,
  Zeven a -> Zodd b -> Zodd (a + b).
 Proof.
-- 
cgit v1.2.3