proposition: Lemma sn4bin' n: \sum_(i<n.+1) i ^4 = (T_nkbin n 1) + 12 * (T_nkbin n 2).
proof: Proof. elim: n => [| n Hrec];first by rewrite big_ord_recl big_ord0 //. rewrite big_ord_recr /= Hrec n4bin'. by rewrite addnCA - addnA - mulnDr addnA (addnC (U_nkbin _ _)) 2!UT_nkbin. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)