proposition: Lemma ribbon_on_box_exE : ribbon_box_ex inner outer = (start, nth 0 inner start).
proof: Proof. by rewrite /ribbon_box_ex -(ribbon_on_startE partinn partout Hrib). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition