proposition: Fact alpha_inc n : α n < α (S n).
proof: Proof. Proof using Hb_nat. destruct n; simpl; try lia. apply inj_lt, alpha_nat_inc. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)