proposition: Lemma Zgcd_mult_rel_prime : forall a b c, Z.gcd a c = 1 -> Z.gcd b c = 1 -> Z.gcd (a*b) c = 1.
proof: Proof. intros. rewrite Zgcd_1_rel_prime in *. apply rel_prime_sym; apply rel_prime_mult; apply rel_prime_sym; auto. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia