proposition: Fact dio_rel_lt r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => r ν < t ν).
proof: Proof. intros H1 H2. by dio equiv (fun ν => exists a b, a < b /\ a = r ν /\ b = t ν). abstract (intros v; split; [ exists (r v), (t v) | intros (? & ? & ? & -> & ->) ]; auto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)