proposition: Lemma coPrimeMult3 (a b c: nat): a > 0 -> b > 0 -> c > 0 -> CoPrime a c -> CoPrime b c -> CoPrime (a * b) c.
proof: Proof. intros H H0 H1 H2 H3; assert (H4: Bezout (Z.of_nat a) (Z.of_nat c) (Z.of_nat 1)). { apply gcd_bezout_nat. assumption. apply H2. } assert (H5: Bezout (Z.of_nat b) (Z.of_nat c) (Z.of_nat 1)). { apply gcd_bezout_nat. assumption. apply H3. } inversion H4 as [x x0 H6]; clear H4. inversion H5 as [x1 x2 H7]; clear H5. split. - exists (Z.of_nat (a * b)). lia. - exists (Z.of_nat c). lia. - intros e [H8 H9]. set (A := Z.of_nat a) in *. set (B := Z.of_nat b) in *. set (C := Z.of_nat c) in *. assert (H10: (1%Z = (A * B * (x * x1) + C * (x0 * B * x1 + x2 * A * x + x0 * x2 * C))%Z)). { change 1%Z with (Z.of_nat 1 * Z.of_nat 1)%Z. rewrite <- H6 at 1. rewrite <- H7. ring; reflexivity. } intros. destruct H4. rewrite H10. apply Z.divide_add_r. + exists (H8 * x * x1)%Z. assert (A * B = Z.of_nat (a * b))%Z by lia. rewrite H5. rewrite H9. lia. + apply Z.divide_mul_l. exists x3. auto. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow