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