proposition: Lemma G5_a r t q: \sum_(i<r.+1) ( 'C(t+r - i, t) * 'C(q + i, q) ) = 'C(q+t+r+1,r).
proof: Proof. move: t; elim:r. by move => t ; rewrite bin0 big_ord_recl /= big_ord0 ! addn0 subn0 !binn. move => n H; elim => [| t H1]. rewrite addn0 addnAC addn1 - binom_mn_n - {1} (addn1 q) - addnA add1n - F23. by apply: eq_bigr => i _;rewrite bin0 mul1n. transitivity ( \sum_(i < n.+1) 'C(t.+1 + n - i, t.+1) * 'C(q + i, q) + \sum_(i < n.+2) 'C(t + n.+1 - i, t) * 'C(q + i, q)). rewrite big_ord_recr (big_ord_recr (n.+1)) /= !addnK !binn !mul1n addnA. congr (_ + _); rewrite - big_split; apply: eq_bigr => i _ /=. rewrite - mulnDl; congr (_ * _); case : i => [j] /=; rewrite ltnS => je. by rewrite - 2! addSnnS - (addnBA _ je) - binS - (addnBA _ je) - addSn. by rewrite H H1 !addn1 -(addnA q t) -(addSnnS t n) (addnA q) addnC (addnS _ n). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)