proposition: Lemma ribbon_startrem inner outer : is_part inner -> is_part outer -> ribbon inner outer -> let min := mindropeq inner outer in let height := ribbon_height inner outer in startrem 0 inner (sumn (outer / inner)) (mindropeq inner outer).-1 = (min - height, nth 0 outer (min - height) - nth 0 inner (min - height)).
proof: Proof. move=> partinn partout Hrib. have /= := ribbon_mindropeq partinn partout Hrib. by move/(ribbon_on_startrem partinn partout) ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition