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