proposition: Lemma fuscj_val n: natp n -> Fuscj n \0c = fusc n.
proof: Proof. move: fusc_pr => [Ha Hb Hc Hd]. by move => nN; rewrite /Fuscj succ_zero Ha Hb (fusci_val nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)