fact: Fixpoint bitsFromInt32S (k: nat)(n: Int32): seq bool := match k with | 0 => [::] | k.+1 => let p := bitsFromInt32S k (lsr n one) in (eq (land n one) one) :: p end.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)