proposition: Lemma prime_div_false : forall a p, prime p -> (a | p) -> 1 < a < p -> False.
proof: Proof. intros a p Pp D Bp. destruct (prime_divisors p Pp a D) as [|[|[|]]]; lia. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts