proposition: Lemma fuscj_even n m: natp n -> natp m -> Fuscj (cdouble n) m = Fuscj n (cdouble m).
proof: Proof. move: fusc_pr => [Ha Hb Hc Hd] nN mN. move: (NS_fusc mN) (NS_fusc (NS_succ mN)) => sa sb. by rewrite /Fuscj (fusci_even nN sb sa) (Hc _ mN) (Hd _ mN) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)