proposition: Lemma shrB_shlB n (p: BITS n.+1) : msb p == false -> shrB (shlB p) = p.
proof: Proof. move => H. apply toNat_inj. rewrite toNat_shrB toNat_shlB. rewrite expnS mul2n. rewrite -!muln2. rewrite -muln_modl => //. have: toNat p < 2^n. apply (proj1 (msb0Bounded _)) => //. move => LT. rewrite modn_small => //. by rewrite muln2 doubleK. 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)