proposition: Lemma add_ribbon_height : hgt = ribbon_height sh res.
proof: Proof. move: is_part_add_ribbon. move: Hret (startrem_leq sh nbox.+1 pos); rewrite /add_ribbon. case: startrem => start [|rem]//= [<- <-] /(_ (lt0n _)) Hstart Hpart. apply: ribbon_on_height => //. exact: add_ribbon_on_remP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition