proposition: Fact alpha_nat_le n : alpha_nat n <= b_nat * alpha_nat (S n).
proof: Proof. Proof using Hb_nat. apply Nat.le_trans with (1*alpha_nat (S n)). + apply Nat.lt_le_incl, Nat.lt_le_trans with (1 := alpha_nat_inc _); lia. + apply Nat.mul_le_mono; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)