proposition: Corollary alpha_nat_smono i j : i < j -> alpha_nat i < alpha_nat j.
proof: Proof. Proof using Hb_nat. intros; apply Nat.lt_le_trans with (1 := alpha_nat_inc _), alpha_nat_mono; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)