fact: Definition joinNibble {n} (p:NIBBLE) (q: BITS n) : BITS (n.+4) := let (p1,b0) := splitlsb p in let (p2,b1) := splitlsb p1 in let (p3,b2) := splitlsb p2 in let (p4,b3) := splitlsb p3 in joinmsb (b3, joinmsb (b2, joinmsb (b1, joinmsb (b0, q)))).
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)