fact: Definition add_ribbon sh nbox pos := let: (start, rem) := startrem 0 sh nbox.+1 pos in if rem > 0 then Some (add_ribbon_on sh start pos rem, (pos - start).+1) else None.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition