proposition: Lemma eq_adj: forall i bs, eq i (bitsToInt16 bs) = (bitsFromInt16 i == bs) .
proof: Proof. move=> i bs. apply/eqInt16P/eqP; intro; subst; auto using bitsFromInt16K, bitsToInt16K. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)