proposition: Lemma hb_strip_included inner outer : hb_strip inner outer -> included inner outer.
proof: Proof. Proof using. elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=. by move=> /andP[/andP[_ ->] /IHinn ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition