proposition: Lemma bitsToInt32K: cancel bitsToInt32 bitsFromInt32.
proof: Proof. move=> bs; apply/eqP; move: bs. by apply/forallP: bitsToInt32K_valid. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)