proposition: Theorem ribbon_textbookE inner outer : is_part inner -> is_part outer -> ribbon inner outer = ribbon_textbook inner outer.
proof: Proof. move=> partinn partout. apply/idP/idP => [Hrib | Htb]. have:= ribbonP partinn partout Hrib => [][start][stop] Hon. rewrite /ribbon_textbook eq_sym ribbon_noneq // ribbon_included //. rewrite (ribbon_on_conn4_skew _ _ Hon) //=. by apply/forallP => [[[r c] /(ribbon_on_no_square _ Hon) /=]]; apply. have Hrib := ribbon_textbook_on partinn partout Htb. apply/ribbonP => //; exists (ribbontb_start partinn partout Htb). by exists (mindropeq inner outer).-1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition