proposition: Lemma add_ribbon_onP : ribbon_on (pos.+1 - hgt) pos sh res.
proof: Proof. move: Hret; rewrite /add_ribbon. case Hstart : startrem => [start rem]; case: ltnP => // lt0rem [eqstart <-]. rewrite subSS subKn; first last. by have:= startrem_leq_pos sh nbox.+1 pos; rewrite Hstart /=. rewrite -eqstart; apply: add_ribbon_on_remP => //. have := startrem_leq sh nbox.+1 pos. by rewrite Hstart; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition