proposition: Lemma coPrimeMult2 : forall a b c : nat, CoPrime a b -> divide a c -> divide b c -> divide (a * b) c.
proof: Proof. intros a b c H H0 [x H1]; assert (H2: divide a x). { eapply coPrimeMult with (1:= H); now rewrite <- H1. } destruct H2 as [x0 H2]; exists x0; subst; ring. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow