proposition: Lemma a'_bound i j (Hi : (2 <= i)%N) : a' (i + j) <= (2 ^ j).-root (a' i).
proof: Proof. elim: j => [|j HIj] //. by rewrite addn0 expn0 root1C. rewrite addnS. have /a'_S Ha : (2 <= i + j)%N by apply: (leq_trans Hi); rewrite leq_addr. apply: le_trans Ha _; rewrite expnS prod_root ?expn_gt0 //. by rewrite ler_rootC ?nnegrE // rootC_ge0 ?expn_gt0. 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