proposition: Lemma bin_mod2_prop2 n k: 'C(n.*2.+1,k.*2) = 'C(n, k) %[mod 2].
proof: Proof. case: k; first by rewrite !bin0. move => k; rewrite doubleS binS -modnDm bin_mod2_prop1 - doubleS. by rewrite bin_mod2_rec2 addn0 modn_mod. 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)