proposition: Theorem Nprime_or_not_prime : forall n, (Nprime n) \/ (~(Nprime n)).
proof: Proof. intros. destruct n. right. apply Nnot_prime_0. destruct n. right. apply Nnot_prime_1. destruct n. left. apply Nprime_intro. auto with arith. intros. destruct H. inversion H. rewrite H1 in H0. apply Nat.lt_irrefl in H0. contradiction. rewrite <- H2 in H0. assert(2<2). apply Nat.le_trans with (S m). auto with arith. auto with arith. apply Nat.lt_irrefl in H3. contradiction. assert(Nat.eqb (Nleast_div (S(S(S n)))) (S(S(S n)))=true -> Nprime (S(S(S n)))). intros. apply Nleast_div_p_prime. auto with arith. apply Nat.eqb_eq. auto. assert(Nat.eqb (Nleast_div (S(S(S n)))) (S(S(S n)))=false -> ~Nprime (S(S(S n)))). intros. assert(Nleast_div (S(S(S n)))<>(S(S(S n)))). apply Nat.eqb_neq. auto. apply not_eq in H1. destruct H1. apply Nleast_div_lt_p_not_prime. auto with arith. auto. assert(Nleast_div (S(S(S n)))<=S(S(S n))). apply Ndiv_le. auto with arith. apply Nleast_div_div. auto with arith. assert(S(S(S n))<S(S(S n))). eapply Nat.le_trans. eapply H1. apply H2. apply Nat.lt_irrefl in H3. intro. auto. destruct (Nat.eqb (Nleast_div (S (S (S n)))) (S (S (S n)))). left. auto. right. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)