proposition: Theorem Nnot_prime_composed : forall n, n > 2 -> ~(Nprime n) -> exists p, exists q, p > 1 /\ q > 1 /\ n = p * q.
proof: Proof. intros. exists(Nleast_div n). assert(Nleast_div n|n). apply Nleast_div_div. auto with arith. destruct H1. exists q. split. apply Nleast_div_gt_1. auto with arith. split. destruct q. rewrite Nat.mul_0_l in H1. rewrite H1 in H. inversion H. destruct q. rewrite Nat.mul_1_l in H1. symmetry in H1. apply Nleast_div_p_prime in H1. apply H0 in H1. contradiction. auto with arith. auto with arith. rewrite Nat.mul_comm. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)