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