proposition: Lemma fusc3: fusc \3c = \2c.
proof: Proof. have ->: \3c = csucc (cdouble \1c) by rewrite /cdouble (cprod1r CS2). by rewrite (fusc_odd NS1) fusc1 succ_one fusc2 csum_11. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)