proposition: Lemma bitsFromInt16_inj: injective bitsFromInt16.
proof: Proof. move=> x y /eqP H. apply/eqInt16P. move: H; apply/implyP. move: y; apply/(forallInt16P (fun y => (bitsFromInt16 x == bitsFromInt16 y) ==> eq x y)). move=> y; apply idP. move: x; apply/forallInt16P; last by apply bitsFromInt16_inj_valid. move=> x; apply idP. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)