proposition: Lemma dio_rel_is_digit c q i y : 𝔻F c -> 𝔻F q -> 𝔻F i -> 𝔻F y -> 𝔻R (fun ν => is_digit (c ν) (q ν) (i ν) (y ν)).
proof: Proof. dio by lemma (fun ν => is_digit_eq (c ν) (q ν) (i ν) (y ν)). Defined.
imports: Arith ZArith List Undecidability.Shared.Libs.DLW.Utils(utils_tac sums rel_iter gcd) Undecidability.H10.Matija(alpha expo_diophantine) Undecidability.H10.Dio(dio_logic)