proposition: Theorem alpha_nat_Pell' b n : 2 <= b -> alpha_nat b n*alpha_nat b n + alpha_nat b (S n) * alpha_nat b (S n) = 1 + b*(alpha_nat b n * alpha_nat b (S n)).
proof: Proof. rewrite Nat.add_comm, (Nat.mul_comm (alpha_nat b n) (alpha_nat b (S n))). apply alpha_nat_Pell. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)