proposition: Lemma shlB_fromNat n m : m < 2^n -> shlB (fromNat (n:=n.+1) m) = fromNat (m.*2).
proof: Proof. move => LT. apply toNat_inj. rewrite toNat_shlB. rewrite toNat_fromNatBounded => //. rewrite toNat_fromNatBounded => //. rewrite div.modn_small => //. by rewrite expnS mul2n ltn_double. by rewrite expnS mul2n ltn_double. rewrite expnS. apply (ltn_trans LT). apply ltn_Pmull => //. apply expn_gt0. 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)