proposition: Theorem Nleast_div_ge_2 : forall n, n > 1 -> Nleast_div n >= 2.
proof: Proof. intros. assert(Nprime (Nleast_div n)). apply Nleast_div_prime. auto. assert(0<=Nleast_div n). auto with arith. apply le_le_S_eq in H1. destruct H1. apply le_le_S_eq in H1. destruct H1. auto. rewrite <- H1 in H0. apply Nnot_prime_1 in H0. contradiction. rewrite <- H1 in H0. apply Nnot_prime_0 in H0. contradiction. Qed.
imports: Coq(Arith Euclid Compare Lia)