proposition: Lemma ribbon_on_addE start stop inner outer : is_part inner -> is_part outer -> ribbon_on start stop inner outer -> add_ribbon_on inner start stop (nth 0 outer start - nth 0 inner start) = outer.
proof: Proof. move=> partinn partout Hrib. have Hstartrem := ribbon_on_startrem partinn partout Hrib. have := Hrib => [[_ _ Hs _]]; rewrite -subn_gt0 in Hs. have := startrem_leq inner (sumn (outer / inner)) stop. rewrite Hstartrem => /(_ Hs) lesmin. apply/eqP/(part_eqP (is_part_add_ribbon_on lesmin partinn Hs Hstartrem) partout) => i. move: Hrib => [Hsi Hsis {}Hs His]. case: (ltnP i start) => [ltistart | lestarti]. by rewrite !nth_add_ribbon_lt_start // His. move: lestarti; rewrite leq_eqVlt => /orP[/eqP Hi|ltstarti]. by rewrite -Hi nth_add_ribbon_start // subnKC // (ltnW Hs). case: i ltstarti => // i /ltnSE ltstarti. case: (ltnP i stop) => [ltis | lesi]. have {ltstarti} Hi : start <= i < stop by rewrite ltstarti ltis. by rewrite !nth_add_ribbon_in // Hsis. by rewrite nth_add_ribbon_stop_lt // Hsi. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition