fact: Definition fromZ {n} (z:Z) : BITS n := match z with | Zpos _ => fromPosZ z | Zneg _ => fromNegZ (Z.pred (Z.opp z)) | _ => zero _ end.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)