proposition: Theorem alpha_nat_Pell b n : 2 <= b -> alpha_nat b (S n)*alpha_nat b (S n) + alpha_nat b n * alpha_nat b n = 1 + b*(alpha_nat b (S n) * alpha_nat b n).
proof: Proof. intros Hb. generalize (alpha_Pell Hb (S n)); intros H; red in H. unfold alpha_Z in H. apply Nat2Z.inj. repeat rewrite Nat2Z.inj_add. repeat rewrite Nat2Z.inj_mul. change (Z.of_nat 1) with (1%Z). rewrite <- H; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)