proposition: Fact dio_rel_True : 𝔻R (fun _ => True).
proof: Proof. by dio equiv (fun _ => exists x, x = 0). abstract (split; try tauto; exists 0; auto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)