proposition: Lemma Odd_div x : Z.Odd x <-> ~(2 | x).
proof: Proof. split. - intros [k ->] [l e]. lia. - intros d. destruct (Z.Even_or_Odd x) as [ [k ->] | ]; auto. destruct d. exists k; lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)