fact: Definition split3 n1 n2 n3 (p: BITS (n3+n2+n1)) : BITS n1 * BITS n2 * BITS n3 := let (hi,lo) := split2 n1 _ p in let (lohi,lolo) := split2 n2 _ lo in (hi,lohi,lolo).
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)