proposition: Lemma cdouble_halfV n: natp n -> n = cdouble (chalf n) \/ n = csucc (cdouble (chalf n)).
proof: Proof. move => nN; case:(p_or_not_p (evenp n)) => h. by left; exact: (half_even h). right; exact: (half_odd (conj nN h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)