diff options
| -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. |