proposition: Lemma w_seq_bound_tail k (Hk : (2 <= k)%N) l : w_seq (k + l) <= w_seq k * a' k ^+ 2.
proof: Proof. apply: le_trans (w_seq_bound Hk l) _; rewrite ler_wpM2l ?w_seq_ge0 //. have -> : a' k ^+ 2 = exp_quo (a k)%:Q 2 (a k). by rewrite /a' /exp_quo -exprM mul1n. rewrite exp_quo_lessn // ?muln_gt0 ?expn_gt0 ?a_pos // ?ler1n ?a_pos //. by rewrite !mulnA leq_mul2r expnS leq_subr orbT. 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