proposition: Lemma ribbon_on_conn4_box_ex b : connect neig4 boxex b.
proof: Proof. have connV (b1 b2 : box) : b1.1 = b2.1 -> connect neig4 b1 b2. wlog Hlog : b1 b2 / b1.2 <= b2.2. case: (leqP b1.2 b2.2) => [H2 |]; first exact. by move=> /ltnW H2 /(_ _ _ H2) H /esym{}/H; rewrite conn4_sym. move Hdr : (b2.2 - b1.2) => dr. elim: dr b1 Hlog Hdr => [| dr IHdr] b1 Hlog. move/eqP; rewrite subn_eq0 => rleq ceq. apply/eq_connect0/val_inj/eqP. have {Hlog rleq} : b1.2 = b2.2 by apply anti_leq; rewrite Hlog rleq. by case: b1 b2 ceq => [[r1 c1] H1] [[r2 c2] H2] /= -> ->. move=> Hdr eq1. have {}Hdr : b2.2 = b1.2.+1 + dr. by move: Hdr => /eqP; rewrite -(eqn_add2l b1.2) addSnnS subnKC // => /eqP. have {Hlog} lt1 : b1.2 < b2.2 by rewrite Hdr leq_addr. have HB: in_skew inner outer (b1.1, b1.2.+1). move: (box_skewP b1) (box_skewP b2); rewrite /in_skew /=. move=>/andP[/leq_trans/(_ (leqnSn _)) -> /= _]. by rewrite eq1=>/andP[_ /(leq_ltn_trans _)]; apply. apply: (@connect_trans _ _ (BoxSkew HB)). apply: connect1 => /=; rewrite mem_pmap_sub /= /neig4 /=. by case: box_skewval => [r c]/=; rewrite !inE eqxx /= orbT. by apply: IHdr; rewrite //= Hdr addKn. move Hb1 : b.1 => r. have : start <= r <= stop. by rewrite -Hb1; exact: (ribbon_on_is_skew _ _ (box_skewP b)). elim: r b Hb1 => [| r IHr] b Hb1. move=> /andP[]; rewrite leqn0 => /eqP Hstart _. by apply: connV; rewrite /= -(ribbon_on_startE partinn partout Hrib) Hstart Hb1. rewrite leq_eqVlt => /andP[/orP[/eqP Hstart _ | ]]. by apply: connV; rewrite /= -(ribbon_on_startE partinn partout Hrib) Hstart Hb1. rewrite ltnS => lesr ltrs. have HB1: in_skew inner outer (r.+1, nth 0 inner r). rewrite /in_skew /=. have Hr1 : start <= r.+1 <= stop by rewrite ltrs andbT (leq_trans lesr). have:= Hr1; rewrite (ribbon_on_nth_leq partinn Hrib) => ltr1. move: Hrib => [_ Hsis _ _]; rewrite (Hsis r) ?lesr //=. rewrite ltnS leqnn andbT. by move: partinn => /is_partP[_]; apply. apply: (@connect_trans _ _ (BoxSkew HB1)); last exact: connV. have HB2: in_skew inner outer (r, nth 0 inner r). by rewrite /in_skew /= leqnn /= -(ribbon_on_nth_leq partinn Hrib) lesr ltnW. apply: (@connect_trans _ _ (BoxSkew HB2)); first last. apply: connect1 => /=; rewrite mem_pmap_sub /= /neig4 /=. by rewrite !inE eqxx !orbT. by apply: IHr; rewrite // lesr ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition