proposition: Lemma shrBn_joinmsb0: forall n (bs: BITS n) k, shrBn (joinmsb0 bs) k = joinmsb0 (shrBn bs k).
proof: Proof. move=> n bs. elim=> [|k IHk]. - by trivial. - rewrite {1}/shrBn iterS -[iter _ _ _]/(shrBn _ _). by rewrite -shrB_joinmsb0 IHk. 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)