proposition: Lemma double_nz n: natp n -> n <> \0c -> (cdouble n <> \0c /\ cdouble n <> \1c).
proof: Proof. move => nN nz; split; first by apply: (cprod2_nz card2_nz nz). by move => h; move:(proj2 (odd_one)) (even_double nN); rewrite -/(cdouble n) h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)