proposition: Lemma a'_S i (Hi : (2 <= i)%N) : a' i.+1 <= sqrtC (a' i).
proof: Proof. have /andP[H1 H2] := Observation_compare_a_a i. rewrite /a' /exp_quo !expr1 !CratrE root_le_x -?rootCX ?rootC_ge0 ?ler0n //. rewrite root_x_le ?rootC_ge0 ?root_x_le ?exprn_ge0 ?ler0n //. rewrite -!natrX ler_nat -expnM. have/leq_trans -> //: (a i.+1 ^ (2 * a i) <= a i ^ (2 * (2 * a i)))%N. by rewrite [(a i ^ _)%N]expnM leq_exp2r ?(ltnW H2) // muln_gt0 /=. rewrite leq_exp2l //; apply: leq_trans (ltnW H1). rewrite -lez_nat -subr_ge0 -subn1 !PoszM -subzn //. set rhs := (X in 0 <= X). have -> : rhs = (a i)%:Z * ((a i)%:Z - 6%:Z) + 1 by lia. rewrite addr_ge0 // mulr_ge0 // subr_ge0. exact/leq_trans/a_grows/Hi. 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