proposition: Lemma fusci_zero a b: natp b -> Fusci \0c a b = b.
proof: Proof. move: fusc_pr => [Ha Hb Hc Hd] /CS_nat bN. by rewrite /Fusci succ_zero Ha Hb cprod0r (cprod1r bN) (csum0l bN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)