proposition: Lemma primes_are_often_odd p : 3 <= p -> prime p -> Z.Odd p.
proof: Proof. intros p3 pp. destruct (Z.Even_or_Odd p) as [[n ->] | ?]; auto. exfalso. apply prime_alt in pp. destruct pp as (_, pp). apply (pp 2). lia. exists n. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)