proposition: Fact alpha_nat_ge_n n : n <= alpha_nat n.
proof: Proof. Proof using Hb_nat. induction n as [ | n IHn ]. + simpl; auto. + apply le_n_S in IHn. apply Nat.le_trans with (1 := IHn), 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)