proposition: Lemma Fib_fusc_bound n (p := \2c ^c n) (v := Fib_fusc (csucc (csucc n))): natp n -> (p <=c v /\ v <=c (cdouble p)).
proof: Proof. rewrite /p/v;move: n {p v}. suff: forall n, natp n -> let v := Fib_fusc_rec (csucc(csucc n)) in let p := \2c ^c n in [/\ p <=c (P v), p <=c (Q v) , P v <=c (cdouble p) & Q v <c (cdouble p)]. by move => H n nN; move: (H n nN) => [pa pb pc pd]. apply: Nat_induction. move:clt_12 cle_12 => ha hb. have cs11:= CS1. rewrite /= (Fib_fusc_recS (NS_succ NS0)) Fib_fusc_rec1; aw. rewrite (csum0r CS1). rewrite cdouble0 cpowx0 succ_zero /cdouble (cprod1r CS2);split; fprops. move => n nN /=. have ssN:= (NS_succ (NS_succ nN)). rewrite (Fib_fusc_recS ssN). set a := P (Fib_fusc_rec (csucc (csucc n))). set b := Q (Fib_fusc_rec (csucc (csucc n))). rewrite pr1_pair pr2_pair; move => [ha hb hc hd]. have cN:= (NS_pow NS2 nN); have c2N:= NS_double cN. have bN:=(NS_lt_nat hd c2N). move: (csum_Mlele ha hb); rewrite csum_nn - (cdouble_pow2 nN) => r2. move /(double_monotone cN bN): (hb) => le1. have r1:=(cleT le1 (cleS (NS_double bN))). move:(csum_Mlelt c2N hc hd);rewrite csum_nn => r4. by move/(double_monotone2 bN c2N): hd; move /(cleSltP (NS_double bN)) => r3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)