proposition: Theorem dio_rel_alpha a b c : 𝔻F a -> 𝔻F b -> 𝔻F c -> 𝔻R (fun ν => 3 < b ν /\ a ν = alpha_nat (b ν) (c ν)).
proof: Proof. dio by lemma (fun v => alpha_diophantine (a v) (b v) (c v)). 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)