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