proposition: Lemma even_odd_factor_uniq n p n' p': natp n -> natp p -> natp n' -> natp p' -> (\2c ^c n) *c csucc (cdouble p) = (\2c ^c n') *c csucc (cdouble p') -> (n = n' /\ p = p').
proof: Proof. wlog: n p n' p'/ n <=c n'. move => H nN pN n'N p'N eq; case: (NleT_ee nN n'N) => h;first by apply: H. by symmetry in eq; move:(H _ _ _ _ h n'N p'N nN pN eq) => [sa sb]. move => nn nN pN n'N p'N. have dN:=(NS_diff n n'N). move:(NS_pow NS2 nN) (NS_pow NS2 dN) (NS_succ (NS_double pN)) => ha hb hc. have hd:=(NS_succ (NS_double p'N)). rewrite -(cdiff_pr nn) cpow_sum2 - cprodA. move /(cprod_eq2l ha hc (NS_prod hb hd) (@cpow2_nz n)). case: (equal_or_not (n' -c n) \0c) => eq. rewrite eq cpowx0 (Nprod1l hd)(Nsum0r nN). move/(csucc_inj (CS_nat (NS_double pN)) (CS_nat (NS_double p'N))). by move/(double_inj pN p'N) => ->. move=> eq2; move:(odd_succ_double pN); rewrite eq2; move => [_]; case. move: (cpred_pr dN eq) => [sa ->]. rewrite - (cdouble_pow2 sa) cprodC double_prod; apply: even_double; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)