proposition: Lemma ribbonP inner outer : is_part inner -> is_part outer -> reflect (exists start stop, ribbon_on start stop inner outer) (ribbon inner outer).
proof: Proof. elim: inner outer=> [/= outer | inn0 inn IHinn]. rewrite orbF => Hinn Hout. apply: (equivP (@ribbon_fromP [::] outer Hinn Hout)). split => [[stop] H | [start] [stop] []]; first by exists 0, stop. case: start => [Hsi Hsis Hs _| start _ _ Hs His]; first last. exfalso; move/(_ 0 (ltn0Sn _)) : His => /= H0. by case: outer H0 Hout Hs => // out0 out +/part_head_non0 => /= ->. by exists stop. case=> [/part_head_non0 /= H0 _| out0 out]. apply (iffP idP) => [] // [start] [stop]. by move=> /ribbon_on_stop_lt; rewrite /= ltn0; apply. move=> partinn partout. have:= partinn => /= /andP[hinn Hinn]. have:= partout => /= /andP[hout Hout]. apply (iffP orP) => [[/andP[lt0]/orP[/eqP Heq|] | /andP[/eqP eq0 Hrib]] | ]. - by exists 0, 0; split => // [][//|i]/=; rewrite Heq. - move=> {IHinn} /=/andP[/eqP eqhout]. move/(ribbon_fromP Hinn Hout) => [stop] [Hsi Hsis Hs His]/=. exists 0, stop.+1. split => //= [] [|i]//=; rewrite ltnS; [exact: Hsi | exact: Hsis]. - move/(_ _ Hinn Hout Hrib) : IHinn => [start] [stop] [Hsi Hsis Hs His]. exists start.+1, stop.+1. split => //= [] [|i]//=; rewrite ltnS; [exact: Hsi | exact: Hsis| exact: His]. - move=> [[/(ribbon_fromP partinn partout) /= ->|start]]; first by left. move=> [stop] Hrib. have := ribbon_on_start_stop Hrib; case: stop Hrib => // stop. rewrite ribbon_onSS => [[/eqP ->]] Hrib _. rewrite ltnn eqxx /=; right. by apply/IHinn => //; exists start, stop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition