proposition: Theorem alpha_diophantine a b c : 3 < b /\ a = alpha_nat b c <-> exists a' b' c', a' = a /\ b' = b /\ c' = c /\ exists u t r s v w x y, alpha_conditions a' b' c' u t r s v w x y.
proof: Proof. split. + exists a, b, c; msplit 3; auto; apply alpha_necessity; auto. + intros (? & ? & ? & -> & -> & -> & H); revert H. intros (u & t & r & s & v & w & x & y & H); revert H. apply alpha_sufficiency. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)