proposition: Lemma G5_b n p q: p <= n -> q <p -> \sum_(q+1 <= k < (n - p + q + 1).+1) ( 'C(n-k, p-q-1) * 'C(k-1, q)) = 'C(n,p).
proof: Proof. move => pa pb. rewrite - (bin_sub pa) - addnA - subnDA addn1. move: (subnK pb); set r := n - p; set t := p - q.+1 => pc. have pd : n = q+t+r+1. by rewrite (addnC _ r) - addnA - (subnK pa) (addnC q) -addnA addn1 pc. rewrite - {1} (add0n (q.+1)) big_addn big_mkord. rewrite (subSn (leq_addl r q.+1)) addnK pd -G5_a. apply:congr_big => // i _; congr (_ * _); last by rewrite addnS subn1 addnC. case i => [m] /=; rewrite ltnS => mr; congr ('C(_, t)). rewrite - (addnBA t mr) (addnC q) -addnA -addnA (addnCA q) addn1. by rewrite - {1} (subnK mr) - addnA addnA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)