proposition: Fact dio_rel_cst x n : 𝔻R (fun ν => ν x = n).
proof: Proof. exists (x ≐ ⌞n⌟); abstract (intro; simpl; tauto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)