proposition: Lemma ribbon_textbook_on : ribbon_on start stop inner outer.
proof: Proof. have start_ltn : nth 0 inner start < nth 0 outer start. by rewrite /start; case: ex_minnP. split => [i|i||i]; first 2 last; first exact: start_ltn. - rewrite /start; case: ex_minnP => m _ Hmin ltim; apply anti_leq. have/includedP := incl => [[_ ->]]; rewrite andbT. by apply/contraLR: ltim; rewrite -leqNgt -ltnNge; exact: Hmin. - have := mindropeq_non0. rewrite /mindropeq; case: ex_minnP => [[//|m]] /eqP Hdrop _ _ /= ltmi. by rewrite -(subnKC ltmi) -!nth_drop Hdrop. have conn4sym : connect_sym neig4 := @conn4_sym _ _. move=> Hi; apply anti_leq; apply/andP; split. move/includedP: incl => [_ /(_ i)]; rewrite leq_eqVlt => /orP[/eqP-> | lti]. by move/is_partP: partout => [_/(_ i)/leq_trans]; apply. have Hb : in_skew inner outer (i, nth 0 inner i) by rewrite /in_skew /= leqnn. move: Htb => /and4P[_ _ _]; rewrite /has_no_square => /forallP/=. move/(_ (BoxSkew Hb)); rewrite /in_skew /=. move/is_partP: partinn => [_/(_ i)/leq_trans->]//=. by rewrite -leqNgt. move: Htb => /and4P[_ _ + _]; rewrite /conn4_skew => /card1P[/= b0] Heq. have {Heq} conn0 (b : box) : root neig4 b = b0. have := Heq (root neig4 b); rewrite !inE /roots root_root // eqxx /=. by move=> /esym/eqP ->. have {conn0 b0}bconn (b1 b2 : box) : connect neig4 b1 b2. by apply/rootP => //; rewrite !conn0. rewrite ltnNge; apply/negP => lti. pose P := [pred b : box | b.1 <= i]. have close4 : closed neig4 P. apply/intro_closed => //= [][[r1 c1] Hrc1] [[r2 c2] Hrc2]. rewrite mem_pmap_sub /= /neig4 !inE /= . move=> /or4P[]/eqP[Hr2 Hc2]; subst r2 c2 => //. by move/(leq_trans (leq_pred _)). move=> ltr1; rewrite (ltn_neqAle _ _) ltr1 andbT. apply/negP => /eqP eqr1; move: lti; rewrite -{ltr1}eqr1. move: Hrc1 Hrc2; rewrite /in_skew /= => /andP[H1 _]/andP[_ H2]. by move/(leq_trans H2)/leq_trans/(_ H1); rewrite ltnn. have Hbstart : in_skew inner outer (start, nth 0 inner start). by rewrite /in_skew /= leqnn start_ltn. pose bstart := BoxSkew Hbstart. have Pstart : P bstart by rewrite /P /=; move: Hi => /andP[]. have Hbstop : in_skew inner outer (stop, nth 0 inner stop). by rewrite /in_skew /= leqnn ribbontb_stop_ltn. pose bstop := BoxSkew Hbstop. have {bconn}/(closed_connect close4) := bconn bstart bstop. move: Pstart; rewrite !inE => -> /esym /=. by move: Hi => /andP[_ /ltn_geF ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition