fact: Definition shift_tests x toNatX y bitsY := allb [:: native_repr (lsr y x) (shrBn bitsY toNatX) ; native_repr (lsl y x) (shlBn bitsY toNatX)].
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic