proposition: Theorem Zeven_ex_iff n : Zeven n <-> exists m, n = 2*m.
proof: Proof. Proof (Zeven_equiv n). Theorem Zodd_ex_iff n : Zodd n <-> exists m, n = 2*m + 1. Proof (Zodd_equiv n). Notation Zeven_bool := Z.even (only parsing). Notation Zodd_bool := Z.odd (only parsing). Lemma Zeven_bool_iff n : Z.even n = true <-> Zeven n. Proof. now rewrite Z.even_spec, Zeven_equiv. Qed.
imports: BinInt