proposition: Lemma binom_half_aux n: natp n -> oddp n -> binom n (chalf n) = binom n (csucc (chalf n)).
proof: Proof. move => nN no; move: (NS_half nN). rewrite {2 4} (half_odd no); set k := chalf n => kN. have ->: (csucc (cdouble k)) = (csucc k) +c k. by rewrite cdoubleE - (csum_Sn _ kN). exact: (binom_symmetric2 (NS_succ kN) kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)