proposition: Lemma bitsFromInt32_bij: bijective bitsFromInt32.
proof: Proof. split with (g := bitsToInt32); auto using bitsToInt32K, bitsFromInt32K. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)