proposition: Lemma Observation_compare_a_a i : (a i).-1 ^ 2 < a (i.+1) < (a i) ^ 2.
proof: Proof. rewrite aS ltnS -!mulnn leq_pmul2r // leq_pred /= -addn1 addSn. have -> : a i * a i = a i * (a i).-1 + a i by rewrite -mulnSr prednK. by rewrite ltn_add2l. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial