proposition: Lemma leibnS m n : 'L(m.+1, n.+1) * 'L(m.+1, n) = 'L(m, n) * ('L(m.+1, n.+1) + 'L(m.+1, n)).
proof: Proof. case: (leqP n m.+1) => H; last first. by rewrite leibn_small 1?ltnW // leibn_small // !muln0. apply/eqP. have /eqn_pmul2l<- : m.+2 * n.+1 > 0 by []. apply/eqP. rewrite -[_.+2 * _ * _]mulnA [n.+1 * _]mulnA. rewrite [in RHS]mulnCA -[_.+2 * _ * _ in RHS]mulnA. rewrite mulnDr leibn_right. rewrite mulnDr [m.+2 * (_.+1 * _) in RHS] mulnCA. rewrite -{1}leibn_up [in RHS]mulnC mulnDl. rewrite -mulnA ['L(_,_) * _]mulnC 2!mulnA. rewrite -mulnDl; congr (_ * _). rewrite [X in _ = X + _]mulnA [X in _ = _ + X]mulnA. rewrite -mulnDl; congr (_ * _). by rewrite [_ * _.+2 in RHS]mulnC -mulnDr addnS subnK. Qed.
imports: mathcomp(all_ssreflect)