proposition: Lemma half_even n: evenp n -> n = cdouble (chalf n).
proof: Proof. move => [nN pb]; move: (cdiv_pr nN NS2); rewrite pb csum0r; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)