proposition: Lemma ribbon_on_nth_leq i : (start <= i <= stop) = (nth 0 inner i < nth 0 outer i).
proof: Proof. apply/idP/idP. - move: Hrib => [_ Hsis Hs _] /andP[]. rewrite leq_eqVlt => /orP[/eqP <-_ // | ]. case: i => // i /ltnSE lesi ltis. rewrite Hsis ?lesi ?ltis // ltnS. by move/is_partP: partinn => [_]; apply. apply: contraLR; rewrite negb_and -!ltnNge ltnS => /orP[|]. - by move: Hrib => [_ _ _ /[apply]->]. - by move: Hrib =>[+ _ _ _] => /[apply] ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition