proposition: Theorem Nleast_div_prime : forall p, p>1 -> Nprime (Nleast_div p).
proof: Proof. intros. split. apply Nleast_div_gt_1. auto. intros. intro. destruct H0. assert((n|p)). apply Ndiv_trans with (Nleast_div p). auto. apply Nleast_div_div. auto with arith. apply Nleast_div_least in H3. apply Nat.lt_irrefl with (Nleast_div p). apply Nat.le_trans with (S n). auto with arith. auto. auto with arith. auto. apply Nat.le_trans with (Nleast_div p). auto. apply Ndiv_le. destruct p. inversion H. auto with arith. apply Nleast_div_div. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)