proposition: Lemma even_odd_dichot n (m := csucc n): natp n -> [\/ m = \1c, (m = cdouble (chalf m) /\ chalf m <=c n) | [/\ m = csucc (cdouble (chalf m)), (chalf m) <=c n & csucc (chalf m) <=c n]].
proof: Proof. move => nN; rewrite /m. have mN:= NS_succ nN. have hN:= NS_half mN. have aa:=(cle_halfSn_n nN). case: (equal_or_not n \0c) => nz; first by constructor 1; rewrite nz succ_zero. case: (cdouble_halfV mN) => mv; first by constructor 2. constructor 3; split => //; apply/(cleSltP hN). apply/(double_monotone2 hN nN) /(cleSltP (NS_double hN)). by rewrite - mv; apply:(cle_Sn_doublen nN nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)