proposition: Fact alpha_nat_inc n : alpha_nat n < alpha_nat (S n).
proof: Proof. Proof using Hb_nat. induction n as [ | n IHn ]; try (simpl; lia). rewrite alpha_nat_fix_2. replace b_nat with (2+(b_nat-2)) by lia. rewrite Nat.mul_add_distr_r. generalize ((b_nat -2)*alpha_nat (S n)); intro; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)