proposition: Lemma hanson : exists K2 : rat, exists K3 : rat, exists N : nat, [/\ 0 < K2, 0 < K3, K2 ^ 3 < 33%:Q & forall n : nat, (N <= n)%N -> (l n)%:Q < K3 * K2 ^ n].
proof: Proof. exists 3%:Q. case: hanson.Hanson.t3 => K [Hpos H]. exists (K.+1)%:Q; exists 0%N. rewrite !ltr0n; split => // n _; apply: le_lt_trans (H n) _. by rewrite -exprnP -natrX -natrM ltr_nat ltn_mul2r expn_gt0 /=. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals) extra_mathcomp extra_cauchyreals tactics shift bigopz arithmetics seq_defs c_props s_props z3seq_props a_props b_props b_over_a_props