proposition: Lemma add_ribbonP : ribbon sh res.
proof: Proof. apply/(ribbonP partsh is_part_add_ribbon). by exists (pos.+1 - hgt), pos; apply: add_ribbon_onP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition