proposition: Lemma shrB_droplsb n (p: BITS n.+1) : shrB (droplsb p) = droplsb (shrB p).
proof: Proof. destruct n. simpl. case/tupleP: p => [b p]. rewrite /droplsb. simpl. by rewrite !beheadCons. by apply toNat_inj. 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)