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