proposition: Theorem Nleast_div_p_prime : forall p, p > 1 -> Nleast_div p = p -> Nprime p.
proof: Proof. intros. destruct p. inversion H. split. auto. intros. destruct H1. intro. apply Nleast_div_least in H3. rewrite H0 in H3. assert(n<n). apply Nat.le_trans with (S p). auto. auto. apply Nat.lt_irrefl in H4. auto. auto. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)