proposition: Lemma Hanson_2 (p n k : nat) : prime p -> trunc_log p n <= beta p n k.
proof: Proof. move => Hprime; case: (posnP n) => [-> | posn]; first by rewrite trunc_logn0. rewrite betaE // logp_sum_floor // logn_prod; last by move=> i; exact: fact_gt0. have -> : \sum_(0 <= i < k) logn p (n %/ a i)`! = \sum_(0 <= i < k) \sum_(j < trunc_log p n) (n %/ a i) %/ p ^ j.+1. apply: eq_bigr => i _; apply: fact_logp_sum_small => //. exact/leq_ltn_trans/trunc_log_ltn/prime_gt1/Hprime/leq_div. have -> : \sum_(0 <= i < k) \sum_(j < trunc_log p n) (n %/ a i) %/ p ^ j.+1 = \sum_(j < trunc_log p n) \sum_(0 <= i < k) (n %/ a i) %/ p ^ j.+1. exact: exchange_big_dep. suff maj j : j < trunc_log p n -> \sum_(0 <= i < k) (n %/ a i) %/ p ^ j.+1 < n %/ p ^ j.+1. rewrite natsumrB; last by case=> i hi _ /=; apply/ltnW/maj. have {1}-> : trunc_log p n = \sum_(j < trunc_log p n) 1 by rewrite sum1_ord. by apply: leq_sum=> [] [i hi] _; rewrite subn_gt0; apply: maj. have {Hprime} lt1p : 1 < p by exact: prime_gt1. rewrite -(leq_exp2l j.+1 _ lt1p) => hj. have {}hj : p ^ j.+1 <= n by apply: leq_trans hj (trunc_logP _ _). have -> : \sum_(0 <= i < k) (n %/ a i) %/ p ^ j.+1 = \sum_(0 <= i < k) (n %/ p ^ j.+1) %/ a i. by apply: eq_bigr=> i; rewrite divnAC. by apply: suminv_lt1; rewrite divn_gt0 // expn_gt0 (ltn_trans _ lt1p). Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial