proposition: Lemma bitsFromInt16P {k} (n: Int16): size (bitsFromInt16S k n) == k.
proof: Proof. elim: k n => // [k IH] n //=. rewrite eqSS //. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)