proposition: Lemma fusc_bound1 n k: k <= 2 ^ n -> fusc k <= fib (n.+1).
proof: Proof. pose p n:= forall k, k <= 2 ^ n -> fusc k <= fib n.+1. suff: forall n, p n /\ p (n.+1) by move => h;exact: (proj1 (h n)). rewrite/p; clear k p n;elim; first by split;case => // [][] // []. move => n [Ha Hb]; split => // k. rewrite fibSS - (odd_double_half k) expn2S; case: (odd k); last first. rewrite leq_double fusc_even => /Hb hb; apply:(leq_trans hb); apply:leq_addr. rewrite ltn_double fusc_odd => sa. move: sa (Hb _ sa) (Hb _ (ltnW sa)). rewrite -(odd_double_half k./2) expn2S; case: (odd k./2). by rewrite - doubleS leq_double fusc_even=> /Ha sa _ sb; apply: leq_add. rewrite (addnC (fib _)) fusc_even ltn_double => /ltnW /Ha sa sb _. by apply: leq_add. 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)