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