proposition: Lemma ribbon_on_stop_lt : stop < size outer.
proof: Proof. case: outer partout Hrib => [_ |out0 out Hpart] [Hsi Hsis Hs His]. by rewrite nth_nil in Hs. rewrite ltnNge; apply/negP => /= Hos. case: (leqP start (size out)) => Hso. have /Hsis : start <= size out < stop by rewrite Hso Hos. by rewrite nth_default. by rewrite [X in _ < X]nth_default in Hs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition