proposition: Lemma ribbon_on_startrem_acc start stop inner outer acc : is_part inner -> is_part outer -> ribbon_on start stop inner outer -> startrem acc inner (sumn (outer / inner)) stop = (acc + start, nth 0 outer start - nth 0 inner start).
proof: Proof. elim: start stop inner outer acc => [|start IHstart] stop inner outer acc. by rewrite addn0; apply: ribbon_on0_startrem. case: outer => [|out0 out]. by move=> _ _ [_ _]; rewrite nth_nil. case: inner => [|inn0 inn]. move=> _ /part_head_non0 => /= Hout0 [_ _ _] /(_ 0 (ltn0Sn _)) /= /eqP. by rewrite (negbTE Hout0). move=> partinn partout. have:= (is_part_ijP _ partout) => [][_ /(_ 0 start.+1 (leq0n _)) /= Hstout0]. move: partinn partout => /=/andP[Hinn0 partinn] /andP[Hout0 partout] Hrib. case: stop Hrib (ribbon_on_start_stop Hrib) => [//|stop]. rewrite ribbon_onSS => [[/eqP H0 Hrib]] _. rewrite H0 subnn add0n {1}(ribbon_on_sumn partinn partout Hrib). have lest : nth 0 out start >= nth 0 inn stop. have:= is_part_ijP _ partinn => [][_]. move=> /(_ _ _ (ribbon_on_start_stop Hrib))/leq_trans; apply. have : included inn out. by apply/ribbon_included/ribbonP => //; exists start, stop. by move/includedP => [_]; apply. rewrite (addnBA _ lest) subnKC; last exact: (leq_trans lest (leq_addl _ _)). rewrite leqNgt addnS ltnS addnC leq_add /= ?leq_subr //. by rewrite IHstart // !(addSn, addnS). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition