proposition: Lemma getBit_shrBn: forall n (bs: BITS n) k k', k + k' < n -> getBit (shrBn bs k) k' = getBit bs (k + k').
proof: Proof. elim=> // n /= IHn /tupleP[b bs] k k' le_kk'. case: k le_kk' => [|k] le_kk' //. have ->: k.+1 + k' = (k + k').+1 by auto with arith. have ->: getBit [tuple of b :: bs] (k + k').+1 = getBit bs (k + k') by compute. rewrite shrBn_Sn shrBn_joinmsb0 /joinmsb0 getBit_joinmsb; last by rewrite (leq_trans (n := k.+1 + k')) // leq_addl //. apply IHn; first by auto with arith. 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)