proposition: Corollary alpha_nat_mono i j : i <= j -> alpha_nat i <= alpha_nat j.
proof: Proof. Proof using Hb_nat. induction 1 as [ | j H1 H2 ]; auto. apply Nat.le_trans with (1 := H2), Nat.lt_le_incl, 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)