proposition: Lemma fusc_bound1 n k: natp n -> k <=c \2c ^c n -> fusc k <=c Fib (csucc n).
proof: Proof. move: n k. suff: forall n, natp n -> (forall k, k <=c \2c ^c n -> fusc k <=c Fib (csucc n)) /\ (forall k, k <=c \2c ^c (csucc n) -> fusc k <=c Fib (csucc (csucc n))). move => H n k ha hb; exact:(proj1 (H n ha) k hb). apply: Nat_induction. have H:forall k, k <c \2c -> fusc k <=c \1c. move => k /clt2; case => ->; rewrite ?fusc0 ?fusc1; fprops; apply: cle_01. rewrite succ_zero succ_one cpowx0 (cpowx1 CS2) Fib1 Fib2; split. by move => k /(cltSleP NS1); rewrite succ_one; apply:H. move => k ke; case: (equal_or_not k \2c) => k2;last by apply:H. by rewrite k2 fusc2; fprops. move => n nN [Hr1 Hr2]; split => // k ka. move:(NS_succ nN) => snN;move:(NS_succ snN) => ssnN. move:(NS_pow NS2 ssnN) (NS_pow NS2 snN)=> pN p1N. have kN:=(NS_le_nat ka pN). have hN:=(NS_half kN). rewrite (Fib_rec snN). case: (cdouble_halfV kN) => sa. move: ka; rewrite sa - (cdouble_pow2 snN) (fusc_even hN). move/(double_monotone hN p1N) /Hr2 => h; apply: (cleT h). apply:(Nsum_Mle0 _ (NS_Fib ssnN)). move: ka; rewrite {2} sa (fusc_odd hN) - (cdouble_pow2 snN) {1} sa. move/(double_le_odd2 hN p1N) => sb; move:(cleT (cleS hN) sb) => sc. move: (Hr2 _ sb) (Hr2 _ sc) => le1 le2. have hhN:=(NS_half hN). case: (cdouble_halfV hN) => ww. move: sc; rewrite {1 2} ww (fusc_even hhN) - (cdouble_pow2 nN). move/(double_monotone hhN (NS_pow NS2 nN)) /Hr1 => sd. exact: (csum_Mlele sd le1). move: sc; rewrite {1 3} ww - (double_succ hhN) - (cdouble_pow2 nN). move/(double_le_odd2 hhN (NS_pow NS2 nN)) /Hr1 => sd. rewrite csumC (fusc_even (NS_succ hhN)); exact: (csum_Mlele sd le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)