Ssreflect Users Discussion List

[Laurent Thery <>]

Hi,

I've formalized the proof pearl

 https://ts.data61.csiro.au/publications/nictaabstracts/9267.pdf

the result can be found here:

http://www-sop.inria.fr/marelle/math-comp-tut-16/MathCompWS/lesson2.html

the binomial library contained all the theorems I needed except two:

forall m n, m.+1 * 'C(m, n) = (m.+1 - n) * 'C(m.+1, n).
forall m n, n.+1 * 'C(m, n.+1) = (m - n) * 'C(m, n).


I was wondering if we could include them to the library and replace :

Lemma mul_Sm_binm m n : m.+1 * 'C(m, n) = n.+1 * 'C(m.+1, n.+1).
Proof.
elim: m n => [|m IHm] [|n] //; first by rewrite bin0 bin1 muln1 mul1n.
by rewrite mulSn {2}binS mulnDr addnCA !IHm -mulnDr.
Qed.

by

Lemma bin_up m n : m.+1 * 'C(m, n) = (m.+1 - n) * 'C(m.+1, n).
Proof.
elim: m n => [|m IHm] [|n] //.
rewrite subSS mulSn {2}binS mulnDr !IHm addnA subSS -mulSn.
case: (leqP m.+1 n)=> [mLn|mLn]; first by rewrite bin_small // muln0 
(eqP mLn).
by rewrite -subSn // -mulnDr -binS.
Qed.

Lemma bin_right m n : n.+1 * 'C(m, n.+1) = (m - n) * 'C(m, n).
Proof.
elim: m n => [|m IHm][|n] //; first by rewrite bin0 bin1 subn0 mul1n muln1.
rewrite [in RHS]binS subSS mulnDr -IHm -mulnDl -mul_Sm_binm.
case: (leqP n m)=> [H|H]; first by rewrite addnS subnK.
by rewrite bin_small ?muln0 // ltnW.
Qed.

so the theorem  mul_Sm_binm is now a direct consequence:

Lemma bin_diag m n : m.+1 * 'C(m, n) = n.+1 * 'C(m.+1, n.+1).
Proof. by rewrite bin_up bin_right. Qed.

--
Laurent