proposition: Lemma ribbon_on_start_le : start <= size inner.
proof: Proof. case: start Hrib => [//|start'] [_ _ Hs His]. rewrite leqNgt; apply/negP => Habs. move/(_ _ Habs) : His; rewrite (nth_default _ (leqnn _)) => Hszinn. case: (ltnP (size inner) (size outer)) => Hsz. by have := nth_part_non0 partout Hsz; rewrite Hszinn. move: Hs; rewrite !nth_default //; apply ltnW => //. exact: (leq_ltn_trans Hsz). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition