proposition: Fact alpha_2 : b = 2 -> forall n, α n = Z.of_nat n - 1.
proof: Proof. Proof using Hb_nat. intros H n. induction on n as IHn with measure n. destruct n as [ | [ | n ] ]; alpha; auto. do 2 (rewrite IHn; try lia). Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)