proposition: Lemma binom_evenP n k: ~~(odd 'C(n,k)) <-> exists i, n %% (2 ^ i) < k %% (2^i).
proof: Proof. have ->: ~~(odd 'C(n,k)) = ('C(n, k) %% 2 == 0). move: (ltn_pmod 'C(n, k) (leqnSn 1)); rewrite {2} (divn_eq 'C(n, k) 2). rewrite oddD muln2 odd_double //=; case: ( _ %% 2) => // [] [] //. move: n {-2} n (leqnn n) k; elim. move => n;rewrite leqn0 => /eqP ->. case; first by split => // [] [i]; rewrite mod0n //. move => k; split => // _; exists k.+1; rewrite mod0n; rewrite modn_small //. by apply: ltn_expl. move => m Hrec n; rewrite leq_eqVlt ltnS;case/orP; last by apply:Hrec. move /eqP => -> k. have ha: (m.+1)./2 <= m by apply: half_le2. move:(Hrec _ ha k./2) => Hc. rewrite - (odd_double_half m.+1) -(odd_double_half k). case:(odd m.+1); case(odd k). + rewrite bin_mod2_prop3; split. by move/Hc => [i]; exists i.+1; rewrite !rem_two_prop2 ltnS ltn_double. move => []; case; first by rewrite !modn1. by move => i; rewrite !rem_two_prop2 ltnS ltn_double => h; apply/Hc; exists i. + rewrite bin_mod2_prop2; split. move/Hc => [i ok]; exists (i.+1). by rewrite rem_two_prop2 rem_two_prop1 -doubleS leq_double. move => []; case; first by rewrite !modn1. move => i; rewrite rem_two_prop2 rem_two_prop1 -doubleS leq_double. by move =>h; apply/Hc; exists i. + rewrite bin_mod2_prop1; split => // _; exists 1; rewrite expn1. by rewrite - !muln2 modnMl addnC modnMDl. + rewrite add0n bin_mod2_rec2; split. by move/Hc => [i ip]; exists i.+1; rewrite add0n !rem_two_prop1 ltn_double. move => [];case; first by rewrite ! modn1. by move => i; rewrite !rem_two_prop1 ltn_double => h; apply/Hc; exists i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)