proposition: Lemma Ncomposed_not_prime : forall n m, 1 < n -> 1 < m -> ~(Nprime (n * m)).
proof: Proof. intros. intro. destruct H1. apply H2 with n. split. auto with arith. replace n with (n*1). destruct n. apply Nat.nle_succ_0 in H. contradiction. rewrite <- Nat.mul_assoc. apply Nat.mul_lt_mono_pos_l; auto with arith. rewrite Nat.mul_1_l. trivial. auto with arith. exists m. ring. Qed.
imports: Coq(Arith Euclid Compare Lia)