proposition: Fact alpha_fix_3 n : α (S (S n)) = b*α (S n) - α n.
proof: Proof. Proof using Hb_nat. destruct n as [ | n ]. 1: simpl; ring. unfold α at 1. rewrite alpha_nat_fix_2. rewrite Nat2Z.inj_sub; auto. rewrite Nat2Z.inj_mul; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)