proposition: Theorem Nprime_least_div_p : forall p, Nprime p -> Nleast_div p = p.
proof: Proof. intros. apply Nprime_least_div_ge_p. destruct p. apply Nnot_prime_0 in H. contradiction. destruct p. apply Nnot_prime_1 in H. contradiction. rewrite <- Nat.sub_succ_l. apply Nat.le_trans with (S (S p)). apply Nat.succ_lt_mono. auto with arith. auto. auto with arith. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)