proposition: Fact alpha_ge_0 n : 0 <= α (S n).
proof: Proof. Proof using Hb_nat. induction n as [ | n IHn ]. + rewrite alpha_fix_1; lia. + apply Z.lt_le_incl, Z.le_lt_trans with (2 := alpha_inc _); trivial. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)