fact: Definition native_repr (i: Int8)(bs: BITS wordsize): bool := eq i (bitsToInt8 bs).
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)