fact: Definition split4 n1 n2 n3 n4 (p: BITS (n4+n3+n2+n1)): BITS n1 * BITS n2 * BITS n3 * BITS n4 := let (b1,rest) := split2 n1 _ p in let (b2,rest) := split2 n2 _ rest in let (b3,b4) := split2 n3 _ rest in (b1,b2,b3,b4).
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)