proposition: Lemma Even_not_Odd x : Z.Even x <-> ~Z.Odd x.
proof: Proof. rewrite Even_div, Odd_div. destruct (Zdivide_dec 2 x); tauto. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)