proposition: Lemma ribbon_on_inj inner outer start1 stop1 start2 stop2 : is_part inner -> ribbon_on start1 stop1 inner outer -> ribbon_on start2 stop2 inner outer -> (start1, stop1) = (start2, stop2).
proof: Proof. move=> partinn H1 H2; congr (_, _). - wlog leq12: start1 start2 stop1 stop2 H1 H2 / start1 <= start2. move=> Hwlog; case: (leqP start1 start2) => [H12 | /ltnW H21]. + exact/(Hwlog _ _ _ _ H1 H2). + exact/esym/(Hwlog _ _ _ _ H2 H1). apply anti_leq; rewrite {}leq12 /=. move: H1 H2 => [_ _ Hs1 _] [_ _ _ His2]. case: leqP => // /His2 Heq. by rewrite Heq ltnn in Hs1. - wlog leq12: start1 start2 stop1 stop2 H1 H2 / stop1 <= stop2. move=> Hwlog; case: (leqP stop1 stop2) => [H12 | /ltnW H21]. + exact/(Hwlog _ _ _ _ H1 H2). + exact/esym/(Hwlog _ _ _ _ H2 H1). apply anti_leq; rewrite {}leq12 /=. move: H1 => [Hsi1 _ _ _]. case: leqP => // {start1 stop1}/Hsi1 => Heq. have:= ribbon_on_start_stop H2. rewrite leq_eqVlt => /orP[/eqP eqss | ltss]. + by move: H2 => [_ _]; rewrite eqss Heq ltnn. + case: stop2 H2 Heq ltss => // stop2 [_ Hsis2 _ _] Heq /ltnSE less. have {}/Hsis2 : start2 <= stop2 < stop2.+1 by rewrite less ltnS /=. rewrite {}Heq => Habs. by move/is_partP : partinn => [_ /(_ stop2)]; rewrite Habs ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition