proposition: Lemma fusci_odd n a b: natp n -> natp a -> natp b -> Fusci (csucc (cdouble n)) a b = Fusci n a (a +c b).
proof: Proof. move: fusc_pr => [Ha Hb Hc Hd] nN aN bN. rewrite /Fusci (Hd _ nN) - (double_succ nN) (Hc _ (NS_succ nN)). by rewrite cprodDl cprodDr - csumA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)