proposition: Lemma F37 n p: p<= n -> (\sum_(k < (n-p).+1) ('C(n, k) *'C(n, p+k))) = 'C(2*n,n-p).
proof: Proof. move => h; move: (subnK h); set q := n - p; move => <-. move: (F36 (q+p)(q +p) q);rewrite addnn - mul2n => <-. apply: eq_bigr; move => [j] /=; rewrite ltnS => jq _. by rewrite addnC - (@bin_sub (p + q) (p + j)) ?leq_add2l // subnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)