proposition: Lemma odd_half n: natp n -> chalf (csucc (cdouble n)) = n.
proof: Proof. move=> nN; move:(NS_double nN) => n2N. have h: cdivision_prop (csucc (cdouble n)) \2c n \1c. split; [ by rewrite (Nsucc_rw n2N) | exact: clt_12]. symmetry; exact: (proj1 (cquorem_pr (NS_succ n2N) NS2 nN NS1 h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)