proposition: Lemma Nprime_ge_2 : forall (p:nat), Nprime p -> 2<=p.
proof: Proof. intros. destruct p. apply Nnot_prime_0 in H. contradiction. destruct p. apply Nnot_prime_1 in H. contradiction. unfold Nprime in H. destruct H. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)