proposition: Fact dio_rel_div_im x y : 𝔻R (fun ν => divides (ν x) (ν y)).
proof: Proof. by dio equiv (fun ν => exists a, ν y = a * ν x). unfold divides; tauto. Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)