proposition: Theorem is_gcd_lcm_mult p q g l : is_gcd p q g -> is_lcm p q l -> p*q = g*l.
proof: Proof. destruct (eq_nat_dec g 0) as [ H0 | H0 ]; intros H1. * subst; apply is_gcd_0 in H1. destruct H1; subst; simpl; auto. * destruct is_gcd_rel_prime with (1 := H1) as (u & v & Hu & Hv & H2). intros H3. rewrite Hu, Hv, (Nat.mul_comm u), <- Nat.mul_assoc; f_equal. rewrite (Nat.mul_comm u), (Nat.mul_comm v), <- Nat.mul_assoc, (Nat.mul_comm v). apply is_lcm_fun with (2 := H3). subst; rewrite (Nat.mul_comm u), (Nat.mul_comm v). apply is_lcm_mult, is_rel_prime_lcm; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)