proposition: Lemma even_odd_factor b: natp b -> b <> \0c -> exists n p, [/\ natp n, natp p & b = (\2c ^c n) *c csucc (cdouble p)].
proof: Proof. move => bN. move:(cleR (CS_nat bN)); move: b bN {- 2} b; apply: Nat_induction. by move => b /cle0. move => n nN Hrec b blen bnz; case:(equal_or_not b (csucc n)) => eq; last first. by apply: Hrec => //; apply /(cltSleP nN). move:(NS_succ nN) => bN; move:(NS_half bN) => hN. case: (cdouble_halfV bN) => eq2; rewrite eq; last first. exists \0c, (chalf (csucc n)); split; fprops; try apply:NS_quo. by rewrite - eq2 cpowx0 (Nprod1l bN). case: (equal_or_not (chalf (csucc n)) \0c) => ne1. by move: eq2; rewrite ne1 cdouble0 => /succ_nz. have le1: (chalf (csucc n)) <=c n. apply /(cltSleP nN);rewrite {2} eq2; apply: (clt_n_doublen (NS_quo _ bN) ne1). move: (Hrec _ le1 ne1) => [m [p [mN pN eq3]]]. exists (csucc m), p; split; fprops. by rewrite eq2 eq3 cprodC - double_prod (cdouble_pow2 mN) cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)