proposition: Theorem expo_diophantine p q r : p = expo r q <-> expo_conditions p q r.
proof: Proof. split; auto. Qed.
imports: Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums) Undecidability.H10.ArithLibs(Zp) Undecidability.H10.Matija(alpha)