proposition: Lemma Fib_fusc_rec_eo n (a := P (Fib_fusc_rec n)) (b := Q (Fib_fusc_rec n)) (a' := P (Fib_fusc_rec (csucc n))) (b' := Q (Fib_fusc_rec (csucc n))): natp n -> ((evenp n -> b' = cdouble a /\ (csucc b') = a') /\ (oddp n -> b' = a'/\ (csucc b') = cdouble a)).
proof: Proof. rewrite /a /b/a'/b'; move: n {a b a' b'}; apply:Nat_induction. rewrite Fib_fusc_rec0 Fib_fusc_rec1; aw; split. by rewrite /cdouble succ_zero cprod0r. by move => [_];move: even_zero. move => n nN. rewrite(Fib_fusc_recS (NS_succ nN)); move: (NS_Fib_fusc_rec (NS_succ nN)). set a := (P (Fib_fusc_rec n)); set a' := (P (Fib_fusc_rec(csucc n))). set b := (Q (Fib_fusc_rec n)); set b' := (Q (Fib_fusc_rec(csucc n))). rewrite !pr1_pair !pr2_pair; move => [_ a'N b'N]. case: (p_or_not_p (evenp n)) => eon. move => [Ha _]; move:(Ha eon)(succ_of_even eon) => [e1 e2] seon. rewrite - e2 (csum_Sn _ b'N) csum_nn (double_succ b'N). by split => //; move:(proj2 seon). move: (conj nN eon) => on. move => [_ Hb]; move:(Hb on)(succ_of_odd on) => [sa sb] esn. by rewrite sa csum_nn; split => //; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)