proposition: Fact is_lcm_fun p q r1 r2 : is_lcm p q r1 -> is_lcm p q r2 -> r1 = r2.
proof: Proof. intros (?&?&?) (?&?&?); apply divides_anti; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)