fact: Definition expo_conditions := r = 0 /\ p = 1 \/ q = 0 /\ 0 < r /\ p = 0 \/ (0 < r /\ q <> 0) /\ exists b m a1 a2 a3, (3 < q+4 /\ a1 = alpha_nat (q+4) (1+r)) /\ (3 < b /\ a2 = alpha_nat b r) /\ (3 < b /\ a3 = alpha_nat b (1+r)) /\ b = a1+q*q+2 /\ m + q*q + 1 = b*q /\ p < m /\ rem (p+b*a2) m = rem (q*a2+a3) m.
imports: Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums) Undecidability.H10.ArithLibs(Zp) Undecidability.H10.Matija(alpha)