proposition: Fact dio_rel_disj R S : 𝔻R R -> 𝔻R S -> 𝔻R (fun ν => R ν \/ S ν).
proof: Proof. intros (fR & H1) (fS & H2); exists (fR ∨ fS). abstract (intro; rewrite df_pred_disj, H1, H2; tauto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)