proposition: Fact rel_prime_mult a b c : is_gcd a c 1 -> is_gcd b c 1 -> is_gcd (a*b) c 1.
proof: Proof. intros H1 H2; msplit 2; try apply divides_1. intros k H3 H4. apply H2; auto. apply is_rel_prime_div with (2 := H3). apply is_gcd_sym in H1. revert H1; apply divides_is_gcd; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)