proposition: Lemma is_part_add_ribbon_on nbox : is_part sh -> rem > 0 -> startrem 0 sh nbox stop = (start, rem) -> is_part res.
proof: Proof. move=> Hpart Hrem Hstartrem. have:= startrem_accP 0 nbox stop Hpart; rewrite {}Hstartrem => /(_ Hrem) Hs. have H0 := notin0_part Hpart. move: Hpart => /is_partP[_ Hsort] /=. rewrite is_part_sortedE; apply/andP; split; first last. move: H0; apply contra; rewrite /add_ribbon_on !mem_cat inE. repeat move=> /orP[]. - exact: mem_take. - by case: rem Hrem => // r _; rewrite addnS. - by move=> /mapP[x _ /eqP]. - exact: mem_drop. - by rewrite mem_nseq => /andP[]. apply/(sortedP 0) => /= i ltiszres. case: (ltnP i.+1 start) => [lti1start | lestarti1]. by rewrite !nth_add_ribbon_lt_start // ?Hsort // (ltn_trans (ltnSn _)). move: lestarti1; rewrite leq_eqVlt => /orP[/eqP Hi|ltstarti1]. rewrite -Hi nth_add_ribbon_start nth_add_ribbon_lt_start ?Hi //. by move: Hs; rewrite Hi /= subn0. move: ltstarti1; rewrite ltnS leq_eqVlt => /orP[/eqP Hi| ltstarti]. rewrite -Hi nth_add_ribbon_start. move: less; rewrite leq_eqVlt => /orP[/eqP|] Hss. - rewrite {2}Hss nth_add_ribbon_stop_lt // Hss. exact: (leq_trans (Hsort stop) (leq_addr _ _)). - rewrite nth_add_ribbon_in ?ltnSn ?Hss //. by case: rem Hrem => // r _; rewrite addnS ltnS leq_addr. case: i ltstarti => // i /ltnSE ltstarti in ltiszres *. case: (ltnP i.+1 stop) => [lti1s | lesi1]. rewrite !nth_add_ribbon_in ?ltnS ?Hsort //. + by rewrite ltstarti (ltn_trans _ lti1s). + by rewrite (leq_trans ltstarti _). rewrite nth_add_ribbon_stop_lt //. move: lesi1; rewrite leq_eqVlt => /orP[/eqP|] ltsi. rewrite nth_add_ribbon_in; last by rewrite ltnS ltstarti ltsi /=. by do 2 apply: (leq_trans (Hsort _)). by rewrite nth_add_ribbon_stop_lt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition