proposition: Lemma ribbon_on_is_skew r c : in_skew inner outer (r, c) -> start <= r <= stop.
proof: Proof. by rewrite ribbon_on_nth_leq /in_skew /= => /andP[/leq_ltn_trans]; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition