proposition: Fact is_rel_prime_mult p q l : is_gcd p q 1 -> is_gcd p l 1 -> is_gcd p (q*l) 1.
proof: Proof. intros H1 H2. destruct p as [ | p ]. + generalize (is_gcd_fun H1 (is_gcd_0l _)) (is_gcd_fun H2 (is_gcd_0l _)). intros; subst; auto. + apply no_common_prime_is_coprime; try lia. do 2 (apply proj2 in H1; apply proj2 in H2). intros k Hk H3 H4. apply prime_div_mult with (1 := Hk) in H4. destruct H4 as [ H4 | H4 ]; [ generalize (H1 _ H3 H4) | generalize (H2 _ H3 H4) ]; intro H5; apply divides_1_inv in H5; subst; destruct Hk; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)