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

1 files changed, 20 insertions, 0 deletions

diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 05716af5f..74e2e6fbf 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.