proposition: Lemma fusci_one a b: natp a -> natp b -> Fusci \1c a b = a +c b.
proof: Proof. move => aN bN; rewrite - succ_zero - (cprod0r \2c) (fusci_odd NS0 aN bN). by rewrite (fusci_zero _ (NS_sum aN bN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)