proposition: Lemma TMi_eq_Tnk2 i j: j <= i -> Mi i j = Tnk2 i j.
proof: Proof. elim:i j => [j | n H [_ |]]; first by rewrite leqn0 => /eqP ->. move:(leq0n n); rewrite leq_eqVlt => /orP; case => np. by rewrite - (eqP np). move:(Tnk2_sum np)(Tnk2_div2 (leq0n n.+1)). rewrite !subn0 !addn0 muln1 muln2 addn1 addn2 => sa sb. have pp: 0 < n.+1`!* (n.+2)`! by rewrite muln_gt0 !fact_gt0. apply/eqP;rewrite /= H // (H _ np) -(eqn_pmul2l pp) sb factS -2! mulnA. by rewrite (mulnA n`!) sa - mul2n mulnA muln2 - factS. move => k kp. rewrite ltnS in kp. move:(kp);rewrite leq_eqVlt => /orP; case => kp1. by rewrite (eqP kp1) Mi_diag Tnk2_nn. move:(kp1);rewrite leq_eqVlt => /orP; case => kp2. by rewrite (eqP kp2) Mi_subdiag Tnk2_Snn addn1. rewrite /= (H _ kp) (H _ kp1) (H _ kp2) - addnn addnA - addnA; apply/eqP. have pp: 0 < (n-k)`! * (n+k.+1+2)`! by rewrite muln_gt0 !fact_gt0. have ea: (n - k)`! = (n-k) * (n - k.+1)`!. rewrite - subn_gt0 in kp1; have eb :=(prednK kp1). by rewrite -{1} eb factS eb subnS. have eb:(n + k.+1 + 2)`! = (n+k.+3)* (n + k + 2)`!. by rewrite 2!addn2 factS !addnS. rewrite - (eqn_pmul2l pp) mulnDr {1} eb mulnCA - mulnA (Tnk2_sum kp1). set t := _ * _. rewrite {1} ea -mulnA - mulnA (mulnA (n - k.+1)`!) (Tnk2_sum kp2). set s := _ * _. have ->: t + s = (n.*2.+2)`! * (k.*2.+3). rewrite /t/s mulnCA (mulnCA (n-k)) -mulnDr -{2} (subnK kp) - addnA !addnS. rewrite addnn -3!addnS (addnC (n - k)) mulnDl -addnA -mulnDr -addSnnS addnn. rewrite -(muln2 (k.*2.+3)) mulnCA -mulnDr 2!addSn -{2} (muln2 k) -mulnDl. by rewrite (subnKC kp) muln2 mulnCA - factSr mulnC. by rewrite - (@Tnk2_div2 n.+1 k.+1) ? ltnS // subSS addSn addn1 addn2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)