proposition: Lemma prime_odd : forall p, 2 <> p -> prime p -> p mod 2 = 1.
proof: Proof. intros p N2 Pp. rem (p mod 2) r Er. pose proof Z_mod_lt p 2 as help_lia. cut (r <> 0). lia. clear help_lia; intros Rn; subst. apply Zmod_divide in Rn; [ | lia ]. refine (N2 (prime_div_prime _ _ _ _ _)); auto. apply prime_2. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts