proposition: Lemma bin_mod2_prop3 n k: 'C(n.*2.+1,k.*2.+1) = 'C(n, k) %[mod 2].
proof: Proof. by rewrite binS -modnDm bin_mod2_prop1 bin_mod2_rec2 add0n 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)