proposition: Lemma shrB_joinmsb0: forall n (bs: BITS n), shrB (joinmsb0 bs) = joinmsb0 (shrB bs).
proof: Proof. case=> [bs|n /tupleP [b bs]]. - by rewrite tuple0. - rewrite /shrB; apply f_equal. have ->: droplsb [tuple of b :: bs] = bs by rewrite /droplsb/splitlsb //= tuple.beheadCons. have ->: joinmsb0 [tuple of b :: bs] = [tuple of b :: joinmsb0 bs] by rewrite /joinmsb0 //= tuple.theadCons tuple.beheadCons. by rewrite /droplsb //= tuple.beheadCons. 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)