proposition: Lemma ribbon_on_no_square r c : in_skew inner outer (r, c) -> ~~ in_skew inner outer (r.+1, c.+1).
proof: Proof. move=> Hrc; have := ribbon_on_is_skew partinn Hrib Hrc => /andP[Hr _]. move: Hrc; rewrite /in_skew /= => /andP[innrc _]. apply/negP => Hrc1. have := ribbon_on_is_skew partinn Hrib Hrc1 => /andP[_ Hr1]. move: Hrc1 => /andP[_ coutr1]. move: Hrib => [_ Hsis _ _]. move: coutr1; rewrite Hsis ?Hr // ltnS => /leq_trans/(_ innrc). by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition