proposition: Lemma dec_repr: forall i bs, native_repr i bs -> native_repr (dec i) (decB bs).
proof: Proof. move=> i ?. rewrite /native_repr eq_adj. move/eqP=> <-. apply/eqInt8P. move: i; apply/forallInt8P; last by apply dec_valid. move=> i; apply/eqInt8P. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)