proposition: Fact add_ribbon_intpartn_spec pos : { res : option ('Pr * nat) | omap val_id res = add_ribbon la nbox pos }.
proof: Proof. case Hrib: (add_ribbon la nbox pos) => [[sh h]|]. - have:= is_part_of_add_ribbon (intpartnP _) Hrib. rewrite sumn_intpartn => Hres. by exists (Some (IntPartN Hres, h)). - by exists None. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition