proposition: Lemma add_ribbon_intpartnE pos : add_ribbon la nbox pos =omap val_id (add_ribbon_intpartn pos).
proof: Proof. by rewrite /add_ribbon_intpartn; case: add_ribbon_intpartn_spec. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition