fact: Definition slice n n1 n2 (p: BITS (n+n1+n2)) : BITS n1 := let: (a,b,c) := split3 n2 n1 n p in b.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)