diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-14 11:37:26 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-14 11:37:26 +0000 |
commit | d7a3d9b4fbfdd0df8ab4d0475fc7afa1ed5f5bcb (patch) | |
tree | 5fff2c4b2c2afa143564f5dd73f7ff6f7c94e417 /theories | |
parent | b5956a6cfce68a70e97620d72c927d190dd49742 (diff) |
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
Diffstat (limited to 'theories')
-rw-r--r-- | theories/ZArith/Zeven.v | 20 |
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. |