proposition: Lemma ribbon_on_box_exP : in_skew inner outer (ribbon_box_ex inner outer).
proof: Proof. rewrite ribbon_on_box_exE /in_skew /= leqnn /=. by rewrite -(ribbon_on_nth_leq partinn Hrib) (ribbon_on_start_stop Hrib) leqnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition