proposition: Lemma fusc_bound2 n k: k <= 2 ^ (n.+1) -> (fusc k <= fib n.+2 ?= iff ((k == (FMe n.+2)) || (k == (FMc n.+2)))).
proof: Proof. move => h; split; [ by apply:fusc_bound1 | apply/idP/idP; last first ]. by case/orP => /eqP ->; rewrite ? FM_fusce_val ?FM_fuscc_val eqxx. pose P n := forall k, k <= 2^n -> fusc k = fib n.+1 -> (k = FMe n.+1) \/ (k = FMc n.+1). move: n k h; suff: forall n, P n /\ P n.+1. move => H n k ha /eqP hb. by case: (proj2 (H n) k ha hb) => ->; rewrite eqxx // orbT. elim; first by split;case => //; case;(try by right); case => //; left. move => n [Ha Hb];split; first by exact. move => k;rewrite /P - (odd_double_half k); case: (odd k); last first. rewrite expn2S leq_double fusc_even => /fusc_bound1 => ha hb. by move: ha; rewrite hb leqNgt fib_smonotone // leqnn. have sp q: q.*2.+1 = FMe n.+2 -> n <> 0. have: odd (q.*2.+1) by rewrite /= odd_double. by case n => // h1 h2; move: h1; rewrite h2. rewrite expn2S ltn_double fusc_odd - (odd_double_half k./2). set q := ((k./2)./2); case:(odd k./2). rewrite - doubleS fusc_even => sa. have sa': q.*2.+1 <= 2 ^ n.+1 by apply: ltnW; rewrite - doubleS. move:(sa); rewrite expn2S add1n leq_double => sb sc. move: (fib_sum_bound (fusc_bound1 sa') (fusc_bound1 sb) sc) => [ea eb]. rewrite - addnn add1n - addnS - doubleS. move:(Ha _ sb eb) (Hb _ sa' ea). case => eqa; case => eqb; rewrite eqb eqa. + by move: (sp _ eqb);case n => // n' _; left; rewrite FM_rece. + move: eqb eqa; rewrite FM_recc2 =>/eqP; rewrite eqSS eqn_double => /eqP->. case n => //; case; [by left | case; [ by right | move => m eq1]]. by move:(FM_ltce m); rewrite - eq1 ltnS ltnNge leq_subr. + move: eqb (sp _ eqb); rewrite - (succnK (q.*2.+1)) - doubleS eqa. case n => //; case; [ by right | case; [ by left |]]. move => n1 /eqP; rewrite FM_rece2; move: (FM_ltce n1). case:(FMe n1.+4) => // m; rewrite addSn doubleS succnK. case:(FMc n1.+4) => // m'; rewrite doubleS succnK eqSS eqn_double. by move => h /eqP h'; move:h; rewrite h' ltnS - addnS ltnNge leq_addr. + by right; move:(FM_recc) => [ _ _ h]; rewrite - h. rewrite add0n => sa. move: (sa); rewrite expn2S ltn_double addnC fusc_even => sb sc. move: (fib_sum_bound (fusc_bound1 sa) (fusc_bound1 (ltnW sb)) sc) => [ea eb]. rewrite - addnn add1n - addSn. move:(Ha _ (ltnW sb) eb) (Hb _ sa ea). case => eqa; case => eqb; rewrite eqb eqa. + by move: (sp _ eqb); case n => // n'; rewrite FM_rece; left. + move: eqb eqa; rewrite FM_recc2 =>/eqP; rewrite eqSS eqn_double => /eqP->. case n => //; case; [by left | case; [ by right | move => m eq1]]. by move:(ltnW(FM_ltce m)); rewrite - eq1 ltnNge leq_subr. + move: eqb (sp _ eqb); rewrite eqa. case n => //; case; [ by right | case; [ by left |]]. move => n1 /eqP; rewrite FM_rece2; move: (FM_ltce n1). case:(FMe n1.+4) => // m. rewrite addSn doubleS succnK eqSS eqn_double ltnS. by move => h /eqP h'; move:h; rewrite h' ltnNge leq_addr. + by right; move:(FM_recc) => [ _ _ h]; rewrite - h. 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)