proposition: Lemma getBit_shlB: forall n (bs: BITS n) k, k > 0 -> k < n -> getBit (shlB bs) k = getBit bs k.-1.
proof: Proof. move=> n bs k gtz_k ltn_k. case: k gtz_k ltn_k=> // k ? ltn_k. rewrite /shlB /shlBaux. rewrite getBit_dropmsb=> //. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)