proposition: Fact is_rel_prime_lcm p q : is_gcd p q 1 -> is_lcm p q (p*q).
proof: Proof. intros H. repeat (split; auto). rewrite Nat.mul_comm; auto. intros k (u & ?) (v & ?); subst. rewrite (Nat.mul_comm u). apply divides_mult_compat; auto. apply is_gcd_sym in H. apply is_rel_prime_div with (1 := H) (k := u). rewrite Nat.mul_comm, H1; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)