proposition: Theorem alpha_Pell n : Pell (α (S n)) (α n).
proof: Proof. Proof using Hb_nat. unfold Pell. generalize (MZ_det_A n). unfold A; simpl; intros H. rewrite <- H. rewrite alpha_fix_3; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)