fact: Definition natural_repr (i: Int8)(n: nat): bool := [exists bs, native_repr i bs && (# n == bs)].
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)