proposition: Lemma add_ribbon_on_remP : rem > 0 -> ribbon_on start stop sh res.
proof: Proof. rewrite /ribbon_on => Hrem; split => [i Hsi | i Hsis || i His]. - exact: nth_add_ribbon_stop_lt. - exact: nth_add_ribbon_in. - by rewrite nth_add_ribbon_start -{1}(addn0 (nth 0 sh start)) ltn_add2l. - exact: nth_add_ribbon_lt_start. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition