proposition: Lemma eq_repr: forall i i' bs bs', native_repr i bs -> native_repr i' bs' -> (eq i i') = (bs == bs').
proof: Proof. move=> i i' bs bs'. rewrite /native_repr. repeat (rewrite eq_adj; move/eqP=> <-). apply/eqInt32P/eqP; intro; subst; auto using bitsFromInt32_inj. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)