proposition: Lemma ribbon_on_included : included inner outer.
proof: Proof. apply/part_includedP => // i. move: Hrib => [Hsi _ _ His]. case: (ltnP stop i) => [/Hsi-> // | {Hsi} leis]. case: (ltnP i start) => [/His-> // | {His} lesi]. by apply/ltnW; rewrite -ribbon_on_nth_leq lesi leis. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition