proposition: Lemma ribbon_from_included inner outer : ribbon_from inner outer -> included inner outer.
proof: Proof. elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=. move=> /andP[/ltnW -> /orP[/eqP -> /= | /andP[_ /IHinn //]]]. exact: included_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition