proposition: Lemma ribbon_included inner outer : ribbon inner outer -> included inner outer.
proof: Proof. elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=. move=> /orP[/andP[lt0] | /andP[/eqP-> /IHinn-> //]]; last by rewrite andbT. move=> /orP[/eqP-> | ]; first by rewrite (ltnW lt0) included_refl. by move=> /andP[_ /ribbon_from_included ->]; rewrite (ltnW lt0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition