proposition: Lemma is_part_add_ribbon : is_part res.
proof: Proof. move: Hret; rewrite /add_ribbon. move: (startrem_leq sh nbox.+1 pos). case Hstartrem : startrem => [start [|rem]]//= /(_ (ltn0Sn _)) lesmin [<- _]. exact: (is_part_add_ribbon_on _ _ _ Hstartrem). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition