proposition: Fact dio_rel_div r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => divides (r ν) (t ν)).
proof: Proof. intros H1 H2. by dio equiv (fun v => exists a b, divides a b /\ a = r v /\ b = t v). abstract (intros v; split; [ exists (r v), (t v) | intros (? & ? & ? & -> & ->) ]; auto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)