fact: Definition lsr_test: bool := forallInt32 (fun i => forallInt32 (fun i' => (toNat (bitsFromInt32 i') <= wordsize) ==> native_repr (lsr i i') (shrBn (bitsFromInt32 i) (toNat (bitsFromInt32 i'))))).
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)