proposition: Lemma fusci_val n: natp n -> Fusci n \1c \0c = fusc n.
proof: Proof. move => nN; move:(CS_nat (NS_fusc nN)) => h. by rewrite /Fusci cprod0l (cprod1l h) (csum0r h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)