proposition: Lemma bitsFromInt16K: cancel bitsFromInt16 bitsToInt16.
proof: Proof. apply: inj_can_sym; auto using bitsToInt16K, bitsFromInt16_inj. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)