proposition: Fact dio_rel_le_im x y : 𝔻R (fun ν => ν x <= ν y).
proof: Proof. by dio equiv (fun ν => exists a, ν y = a + ν x). abstract (intros v; split; [ intros H; exists (v y - v x); lia | intros (? & ->); lia ]). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)