proposition: Fact dio_rel_alpha_size : df_size_Z (proj1_sig dio_rel_alpha_example) = 1445%Z.
proof: Proof. reflexivity. Qed.
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)