proposition: Lemma binom_evenP n k: natp n -> natp k -> (evenp (binom n k) <-> exists2 i, natp i & n %%c (\2c ^c i) <c k %%c (\2c ^c i)).
proof: Proof. move => nN kN. have aux:evenp (binom n k) <-> (binom n k) %%c \2c = \0c. split; [by move => [] | move => h; split => //; exact:(NS_binom nN kN)]. apply: (iff_trans aux); clear aux. have Ha:=(crem_of_zero NS2). have Hb:= (crem_small NS2 clt_12). move: n nN {-2} (n) (cleR (CS_nat nN)) k kN. apply: Nat_induction. move => n /cle0 -> k kN. case: (equal_or_not k \0c) => kz. rewrite kz binom00 - Hb; split; first by move:card1_nz. by move => [i iN]; rewrite (crem_of_zero (NS_pow NS2 iN)) => [] [_]. move/(strict_pos_P1 kN): kz => kp. rewrite (binom_bad NS0 kN kp) Ha; split => // _. exists k => //; rewrite (crem_of_zero (NS_pow NS2 kN)). by rewrite - (crem_small (NS_pow NS2 kN) (cantor (CS_nat kN))). move => m mN Hrec n lemn k kN. case:(equal_or_not n (csucc m)) => emn; last first. by apply: Hrec => //; apply /(cltSleP mN). move: (NS_succ mN); rewrite - emn => nN. move: (NS_half nN) (NS_half kN) => hnN hkN. have ha: chalf n <=c m. apply /(cltSleP mN); rewrite - emn;case: (cdouble_halfV nN) => nv. rewrite {2} nv; apply:(clt_n_doublen hnN) => bad. by case: (@succ_nz m); rewrite -emn nv bad cdouble0. rewrite {2} nv;apply/(cltSleP (NS_double hnN)); apply :(cle_n_doublen hnN). have aux: forall i, natp i -> natp (chalf n %%c \2c ^c i) /\ natp (chalf k %%c \2c ^c i). by move => i iN; move: (NS_pow NS2 iN) => h; split; apply: NS_rem. have aux2: forall i, natp i -> i %%c \2c ^c \0c = \0c. move => i iN; rewrite cpowx0; exact: (proj33 (cdivides_one iN)). have Hc:=(Hrec _ ha _ hkN). case: (cdouble_halfV nN);case: (cdouble_halfV kN) => kv nv. + rewrite kv nv (bin_mod2_rec2 hnN hkN); split. move/Hc => [i iN ip]; move: (NS_succ iN) => siN;exists (csucc i); first exact. move:(aux _ iN) => [pa pb]. rewrite(rem_two_prop1 hnN iN) (rem_two_prop1 hkN iN). by apply /double_monotone2. move => [i iN ip]; apply/Hc; case: (equal_or_not i \0c) => eiz. by move: (proj2 ip); rewrite eiz -nv -kv (aux2 _ nN) (aux2 _ kN). move:(cpred_pr iN eiz) => [sa sb]; exists (cpred i); first exact. move:(aux _ sa) => [pa pb]. move: ip; rewrite {1 2} sb (rem_two_prop1 hnN sa) (rem_two_prop1 hkN sa). by move/(double_monotone2 pa pb). + rewrite kv nv (bin_mod2_prop1 hnN hkN) - kv. split. move => _; exists \1c; [ apply: NS1 |rewrite (cpowx1 CS2)]. rewrite(proj2 (even_double (NS_half nN))). have /oddp_alt[_ ->]:oddp k by rewrite kv; apply:(odd_succ_double hkN). apply: clt_01. rewrite - nv; split => //; apply:(NS_binom nN kN). + rewrite kv nv (bin_mod2_prop2 hnN hkN); split. move/Hc => [i iN ip]; move: (NS_succ iN) => siN;exists (csucc i); first exact. * move:(aux _ iN) => [pa pb]. rewrite(rem_two_prop2 hnN iN) (rem_two_prop1 hkN iN). by apply /double_monotone3. move => [i iN ip]; apply/Hc; case: (equal_or_not i \0c) => eiz. by move: (proj2 ip); rewrite eiz -nv -kv (aux2 _ nN) (aux2 _ kN). move:(cpred_pr iN eiz) => [sa sb]; exists (cpred i); first exact. move:(aux _ sa) => [pa pb]. move: ip; rewrite {1 2} sb (rem_two_prop2 hnN sa) (rem_two_prop1 hkN sa). by move/(double_monotone3 pa pb). + rewrite kv nv (bin_mod2_prop3 hnN hkN); split. move/Hc => [i iN ip]; move: (NS_succ iN) => siN;exists (csucc i). exact. move:(aux _ iN) => [pa pb]. rewrite(rem_two_prop2 hnN iN) (rem_two_prop2 hkN iN). apply /(cltSSP (CS_nat (NS_double pa)) (CS_nat (NS_double pb))). by apply /double_monotone2. move => [i iN ip]; apply/Hc; case: (equal_or_not i \0c) => eiz. by move: (proj2 ip); rewrite eiz -nv -kv (aux2 _ nN) (aux2 _ kN). move:(cpred_pr iN eiz) => [sa sb]. exists (cpred i); first exact. move:(aux _ sa) => [pa pb]. move: ip; rewrite {1 2} sb (rem_two_prop2 hnN sa) (rem_two_prop2 hkN sa). move/(cltSSP (CS_nat (NS_double pa)) (CS_nat (NS_double pb))). by move/(double_monotone2 pa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)