proposition: Lemma Odd_not_Even x : Z.Odd x <-> ~Z.Even 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)