proposition: Lemma fuscj_one n: natp n -> Fuscj \1c n = Fuscj \0c (csucc (cdouble n)).
proof: Proof. move => nN. by rewrite - succ_zero - {1} (cprod0r \2c) (fuscj_odd NS0 nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)