proposition: Theorem Nleast_div_lt_p_not_prime : forall n, n > 2 -> (Nleast_div n) < n -> ~(Nprime n).
proof: Proof. intros. intro. assert((Nleast_div n|n)). apply Nleast_div_div. auto with arith. destruct H2. destruct q. rewrite Nat.mul_0_l in H2. rewrite H2 in H. inversion H. destruct q. rewrite Nat.mul_1_l in H2. rewrite <- H2 in H0. apply Nat.lt_irrefl in H0. auto. apply (Ncomposed_not_prime (S(S q)) (Nleast_div n)). auto with arith. apply Nleast_div_gt_1. auto with arith. rewrite H2 in H1. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)