proposition: Lemma half_odd n: oddp n -> n = csucc (cdouble (chalf n)).
proof: Proof. move/oddp_alt => [nN on]. move: (cdiv_pr nN NS2). by rewrite on Nsucc_rw //; apply: NS_double; apply:NS_half. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)