proposition: Lemma doubleS_nz n: natp n -> n <> \0c -> (csucc (cdouble n) <> \0c /\ csucc (cdouble n) <> \1c).
proof: Proof. move => nN nz; split; first by apply: succ_nz. rewrite - succ_zero; move/(csucc_inj (CS_nat (NS_double nN)) CS0). apply: (cprod2_nz card2_nz nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)