proposition: Theorem t2_rat n k (Hank : (a k <= n < (a k.+1))%N) : (C n k.+1)%:Q < (10%:Q * n%:Q) ^ k.+1 * (w ^+ n.+1).
proof: Proof. suff : (C n k.+1)%:Q%:C < exp_quo (10%:Q * n%:Q) (2 * k.+1) 2 * w%:C ^+ n.+1. by rewrite /exp_quo exprM sqrtCK -!rmorphXn /= -rmorphM /= ltr_rat. apply: lt_le_trans (t2 Hank) _; apply: ler_wpM2r. by rewrite exprn_ge0 ?ler0q. case: n {Hank} => [| n]; first by rewrite mulr0 !exp_quo_0 /= mulnC muln2. by apply: exp_quo_lessn=> //; [ring_lia | lia]. 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