proposition: Lemma hb_strip_size inner outer : hb_strip inner outer -> size inner <= size outer <= (size inner).+1.
proof: Proof. Proof using. elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=. by move=> /eqP ->. by move=> /andP[_ /IHinn]; rewrite !ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition