proposition: Lemma fusc_lower_bound n: n.*2 < 2 ^ fusc n.*2.+1.
proof: Proof. have T k: k != 0 -> 1 < 2 ^ (fusc k). by rewrite -[1]/(2^0) ltn_exp2l // lt0n fusc_eq0. elim /fusc_ind :n => //. move => n H; rewrite fusc_odd expnD fusc_even; case nz: (n == 0). by rewrite (eqP nz). apply: (@leq_trans (2 * 2 ^ fusc n.*2.+1)); first by rewrite mul2n ltn_double. by rewrite leq_pmul2r ? expn_gt0 // T // nz. case => // n H _. rewrite fusc_odd expnD - doubleS fusc_even. apply: (@leq_trans (2 ^ fusc (n.+1).*2.+1 * 2)). rewrite muln2 ltn_double - doubleS; move: H; case: (fusc (n.+1).*2.+1) => //. by move => m; rewrite expn2S ltn_double leq_double. rewrite leq_pmul2l ? expn_gt0 // T //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)