proposition: Lemma remark_t2_1 n k (Hank : (a k <= n < a k.+1)%N) : (expn n n)%:Q%:C <= n%:Q%:C * exp_quo n%:Q (n * (a k.+1).-2) ((a k.+1).-1).
proof: Proof. have n_ge1 : (1 <= n)%N by apply: leq_trans (a_pos k) _; lia. rewrite -{3}[n]expn1 !exp_quo_nat_nat -exp_quo_plus ?ler0n // mul1n muln1. rewrite exp_quo_lessn ?ler1n //; nia. 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