proposition: Lemma bin_mod2_rec2 n k: 'C(n.*2,k.*2) = 'C(n, k) %[mod 2].
proof: Proof. case:k; [ by rewrite !bin0 | elim:n; first by move => k; rewrite !bin0n]. move => n Hrec k; rewrite doubleS doubleS bin_mod2_rec1 -doubleS. rewrite - modnDm Hrec; case: k; first by rewrite bin0 !bin1 modnDm addn1. by move => k; rewrite Hrec modnDm binS. 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)