proposition: Theorem Nrel_prime_mult_compat : forall p n m, Nrel_prime p n -> Nrel_prime p m -> Nrel_prime p (n * m).
proof: Proof. intros. intro. intros. destruct n0. destruct H1. rewrite Nat.mul_0_r in H1. rewrite H1 in H. destruct H2. rewrite Nat.mul_0_r in H2. apply Nat.eq_mul_0 in H2. destruct H2. rewrite H2 in H. apply H. apply Ndiv_n_n. apply Ndiv_n_n. rewrite H1 in H0. rewrite H2 in H0. apply H0. apply Ndiv_n_n. apply Ndiv_n_n. destruct n0. auto. assert(exists pn0, Nprime pn0 /\ (pn0|(S(S n0)))). apply Nhas_prime_divisor. auto with arith. destruct H3. destruct H3. assert((x|n*m)). eapply Ndiv_trans. eapply H4. apply H2. apply Ngauss_prime in H5. assert(x=1). destruct H5. apply H0. eapply Ndiv_trans. eapply H4. apply H1. apply H5. apply H. eapply Ndiv_trans. eapply H4. apply H1. apply H5. rewrite H6 in H3. apply Nnot_prime_1 in H3. contradiction. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)