proposition: Fact divides_anti x y : x div y -> y div x -> x = y.
proof: Proof. intros (p & H1) (q & H2). rewrite H1, Nat.mul_assoc in H2. apply own_multiple in H2. destruct H2 as [ H2 | H2 ]. + subst; rewrite Nat.mul_comm; auto. + apply mult_is_one in H2; destruct H2; subst; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)