proposition: Lemma add_ribbon_intpartnP pos res h : add_ribbon_intpartn pos = Some (res, h) -> add_ribbon la nbox pos = Some (val res, h).
proof: Proof. by move/(congr1 (omap val_id)); rewrite add_ribbon_intpartnE /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition