proposition: Lemma Fib_fusc_rec_frec n (F := fun k => (fusc (Fib_fusc k))) : natp n -> F (csucc (csucc n)) = F (csucc n) +c F n.
proof: Proof. move => nN; rewrite /F /Fib_fusc. rewrite (Fib_fusc_recS (NS_succ nN)); aw. move:(Fib_fusc_rec_eo nN)(NS_Fib_fusc_rec (NS_succ nN)) (NS_Fib_fusc_rec nN). set b := Q _; set a := P _; set a' := P _. move => [ce co] [_ a'N bN][_ aN _]. rewrite (fusc_odd bN); case: (p_or_not_p (evenp n)) => en. by move:(ce en) => [{2} -> ->]; rewrite (fusc_even aN) csumC. by move:(co (conj nN en)) => [{2} -> ->]; rewrite (fusc_even aN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)