proposition: Lemma bin_mod2_prop1 n k: 'C(n.*2,k.*2.+1) %%2 = 0.
proof: Proof. elim:n k =>[k | n Ihn [|k]]; first by rewrite bin0n. by rewrite bin1 -mul2n modnMr. by rewrite !doubleS bin_mod2_rec1 -modnDm -doubleS Ihn Ihn. 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)