proposition: Lemma ribbon_on_sumn : sumn (outer / inner) = (stop - start) + (nth 0 outer start - nth 0 inner stop).
proof: Proof. rewrite (sumn_diff_shape ribbon_on_included). have /sumn_nth_le -> := size_included ribbon_on_included. rewrite (sumn_nth_le (leqnn (size outer))). have [Hsi Hsis Hs His] := Hrib. rewrite (big_cat_nat _ (n := stop.+1)) ? ribbon_on_stop_lt //= addnC big_nat. under [X in X + _ - _ = _]eq_bigr => i /andP[+ _] do move/Hsi->. rewrite -big_nat {Hsi} [X in _ - X](big_cat_nat _ _ _ _ ribbon_on_stop_lt) //=. rewrite addnC [X in _ - X]addnC subnDA addnK. have:= ribbon_on_start_stop; rewrite -ltnS => /ltnW less1. rewrite (big_cat_nat _ (n := start)) //=. rewrite big_nat (eq_bigr _ His) {His} -big_nat. rewrite [X in _ - X](big_cat_nat _ (n := start)) //=. rewrite addnC subnDA addnK. have:= ribbon_on_start_stop; rewrite leq_eqVlt => /orP[/eqP Hss | ltss]. by rewrite Hss !big_nat1 subnn add0n. rewrite big_nat_recl ?(ltnW ltss) //. rewrite big_nat (eq_bigr _ Hsis) -big_nat. under eq_bigr do rewrite -add1n. rewrite big_split /= big_nat_recr ?(ltnW ltss) //= addnA subnDA addnK. rewrite addnC sum_nat_const_nat muln1. move/is_part_ijP : partinn => [_ /(_ _ _ (ltnW ltss))]. by move=> /leq_trans/(_ (ltnW Hs))/addnBA ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition