proposition: Lemma l10 n k (Hank : (a k <= n)%N) : (C n k.+1)%:Q%:C < (n ^ n)%N%:Q%:C * \prod_(i < k.+1) exp_quo (10%:Q * n%:Q / (a i)%:Q) (a i).-1 (a i) / \prod_(i < k.+1) exp_quo (n%:Q / (a i)%:Q) n (a i).
proof: Proof. have lt0n : (0 < n)%N by exact: leq_trans (a_pos k) _. have Hinterm : (C n k.+1)%:~R <= ((n ^ n)%N%:~R / (\prod_(i < k.+1) (n %/ a i) ^ (n %/ a i))%N%:~R) :> algC. rewrite ler_pdivlMr. by move: (l8 n k.+1); rewrite big_mkord mulrC -natrM ler_nat. by rewrite ltr0n prodn_gt0 // => i; rewrite expn_gt0; case: (n %/ a i)%N. rewrite !ratr_int -mulrA; apply: le_lt_trans Hinterm _. rewrite ltr_pM2l ?ltr0n ?expn_gt0 ?lt0n //= ltr_pdivlMr; last first. apply: prodr_gt0 => i _. by rewrite exp_quo_gt0 ?divr_ge0 ?divr_gt0 ?ltr0n ?a_pos. rewrite prodMz /= mulrC -prodf_div. apply: ltr_prod; first by apply/hasP; exists ord0; rewrite // mem_index_enum. move=> [i /= Hi] _; rewrite divr_ge0 ?exp_quo_ge0 ?a_pos ?divr_ge0 ?ler0n //=. suff/l7: (a i <= n)%N by rewrite !CratrE subn1. exact/leq_trans/Hank/a_grows. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis