proposition: Lemma F37bis p q: \sum_(k<q.+1) 'C(p+q,k) * 'C(p+q,p+k) = 'C((p+q).*2,q).
proof: Proof. pose f p q := \sum_(k<q.+1) 'C(p+q,k) * 'C(p+q,p+k). pose g p q := 'C((p + q).*2, q). rewrite -/(f p q) - /(g p q); move: p q. have fp0: forall p, f p 0 = 1. by move => p; rewrite /f big_ord_recl big_ord0 binn bin0. have gp0: forall p, f p 0 = g p 0. by move => p; rewrite /g bin0 fp0. have fp1: forall p, f p 1 = (p.+1).*2. move => m; rewrite /f big_ord_recl big_ord_recl big_ord0 binn bin0. rewrite mul1n muln1 addn0 /= /bump /= addn0 addn0. have r1: m = (m + 1) - 1 by rewrite addn1 subn1 -pred_Sn. rewrite {2} r1 -addnn addn1 bin_sub // bin1 //. have gp1: forall p, f p 1 = g p 1. by move => p; rewrite /g bin1 fp1 addn1. have f0q: forall q, f 0 q = 'C(q.*2,q). move=> q; rewrite /f add0n -F38; apply: congr_big => // [[i isn]]. have g0a: forall q, f 0 q = g 0 q. by move => q; rewrite /g f0q. have gp2: forall p q, g p.+1 q.+2 = g p q.+2 + ( g p.+1 q.+1).*2 + g p.+2 q. move => p q; rewrite /g. have ->: (p.+1 + q.+2).*2 = (p.+1 + q.+1).*2.+2. by rewrite -doubleS; congr (double _); rewrite addnS. rewrite binS binS -addnA -addnA addSnnS; congr (_ + _). rewrite -[in X in _ = X + _] addnn -addnA; congr (_ + _). by rewrite binS addSnnS addSnnS. suff fp2: forall p q, f p.+1 q.+2= f p q.+2 + (f p.+1 q.+1).*2 + f p.+2 q. pose aux q:= forall p, f p q = g p q. have aux2: forall q, aux q /\ aux q.+1. elim => [// | n [hr1 hr2]]; split => //. by elim => // => p hrec; rewrite gp2 fp2 hr1 hr2 hrec. move => p q; move: p. move: (aux2 q) => [] //. move=> p q. rewrite /f. rewrite 4! addSn 2! addnS; set n:= (p+q).+2. set t0 := \sum_ (k < q.+3) _; set t1 := \sum_ (k < q.+3) _. set t2 := \sum_ (k < q.+2) _; set t3 := \sum_ (k < q.+1) _. rewrite /t0 big_ord_recl bin0 mul1n /ord0 addn0 binS. set t4 := \sum_(i < q.+2) _. have : t4 = \sum_(i < q.+2) ( ('C(n, i.+1) * 'C(n.+1, (p+i).+2)) + ('C(n,i)) * 'C(n.+1, (p+i).+2)). rewrite /t4; apply: congr_big => // [[i lin]] _ /=. by rewrite /bump /= add1n addSn addnS binS mulnDl. rewrite big_split /=. set t5:= \sum_(i < q.+2) _; set t6 := \sum_(i < q.+2) _; move => r1. have: t5 = \sum_(i < q.+2) (('C(n, i.+1) * 'C(n, (p + i).+2)) + ( 'C(n, i.+1) * 'C(n, (p + i).+1))). rewrite /t5;apply: congr_big => // [[i lin]] _ /=. by rewrite binS mulnDr. have : t6 = \sum_(i < q.+2) (('C(n, i) * 'C(n, (p + i).+2)) + ( 'C(n, i) * 'C(n, (p + i).+1))). rewrite /t5;apply: congr_big => // [[i lin]] _ /=. by rewrite binS mulnDr. rewrite big_split /= big_split /=. set t7:= \sum_(i < q.+2) _; set t8:= \sum_(i < q.+2) _. set t9:= \sum_(i < q.+2) _; set t10:= \sum_(i < q.+2) _. have -> : t8 = t2. rewrite /t2 /t8; apply: congr_big => // [[i lin]] _ /=. have ->: t7 = t3. rewrite /t3 /t7; rewrite big_ord_recr /=. rewrite addnS -/n (bin_small (ltnSn n)) muln0 addn0. apply: congr_big => // [[i lin]] _ /=. rewrite r1 => -> ->. rewrite - [in X in _ = X] addnA (addnC t9) -(addnA t10). rewrite addnCA (addnC ('C(n, p.+1))) -(addnA 'C(n, p)) addnA; congr ( _ + _). rewrite addnC /t1 big_ord_recl bin0 mul1n addn0; congr (_ + _). rewrite /t10; apply: congr_big => // [[i lin]] _ /=. by rewrite /bump /= add1n addnS. rewrite addnA - addnn - (addnA t2) (addnC t3); congr ( _ + _). rewrite /t9 / t2 big_ord_recr /=. rewrite addnS -/n (bin_small (ltnSn n)) muln0 addn0. symmetry; rewrite big_ord_recl bin0 mul1n addn0; congr (_ + _). apply: congr_big => // [[i lin]] _ /=. by rewrite /bump /= add1n addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)