proposition: Theorem Nhas_prime_divisor : forall n, n > 1 -> exists p, Nprime p /\ (p | n).
proof: Proof. intros. exists (Nleast_div n). split. apply Nleast_div_prime. auto. apply Nleast_div_div. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)