proposition: Fact alpha_nat_power n : 2 < b_nat -> power n (b_nat-1) <= alpha_nat (S n) <= power n b_nat.
proof: Proof. Proof using Hb_nat. intros Hb. induction on n as IHn with measure n. destruct n as [ | [ | n ] ]. + do 2 rewrite power_0; simpl; lia. + do 2 rewrite power_1; simpl; lia. + rewrite alpha_nat_fix_2. destruct (IHn n) as (H1 & H2); try lia. destruct (IHn (S n)) as (H3 & H4); try lia. split. * replace b_nat with (b_nat-1+1) at 2 by lia. rewrite Nat.mul_add_distr_r. rewrite <- (Nat.add_sub_assoc (_*_)). - apply Nat.le_trans with (2 := Nat.le_add_r _ _). rewrite power_S; apply Nat.mul_le_mono; auto. - rewrite Nat.mul_1_l; apply alpha_nat_mono; lia. * rewrite power_S. apply Nat.le_trans with (1 := Nat.le_sub_l _ _). apply Nat.mul_le_mono_l; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)