proposition: Lemma n6bin' n: n ^6 = (U_nkbin n 0) + 60* (U_nkbin n 1)+ 360 * (U_nkbin n 2).
proof: Proof. rewrite n6bin -(mul1n (U_nkbin n 0)) -(mulnA 30 2) -(mulnA 120 3). by rewrite - 3! U_nkbin_pr 2! mulnA addn0 addn1 addn2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)