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