proposition: Theorem Nprime_or_composed : forall n, n > 2 -> (Nprime n) \/ (exists p, exists q, p > 1 /\ q > 1 /\ n=p * q).
proof: Proof. intros. assert(Nprime n \/ ~Nprime n). apply Nprime_or_not_prime. destruct H0. left. auto. right. apply Nnot_prime_composed. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)