proposition: Lemma ribbon_on_startrem start stop inner outer : is_part inner -> is_part outer -> ribbon_on start stop inner outer -> startrem 0 inner (sumn (outer / inner)) stop = (start, nth 0 outer start - nth 0 inner start).
proof: Proof. move/ribbon_on_startrem_acc => H{}/H H{}/H ->. by rewrite add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition