proposition: Fact dio_rel_add_sym x y z : 𝔻R (fun ν => ν y + ν z = ν x).
proof: Proof. dio_sym (dio_rel_add x y z). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)