proposition: Lemma nth_add_ribbon_in i : start < i.+1 <= stop -> nth 0 res i.+1 = (nth 0 sh i).+1.
proof: Proof. move=> /andP[ltsi leis]. rewrite /add_ribbon_on nth_cat size_take. rewrite -/(minn _ _) (minn_idPl lessz) ltnNge (ltnW ltsi) /=. rewrite subSn //= nth_cat size_map sztd. rewrite ltn_subRL subnKC // leq_min leis /=. case: ltnP => [ltisz | leszi]. - rewrite (nth_map 0); first last. by rewrite sztd ltn_subRL subnKC // leq_min leis. by rewrite nth_drop subnKC // nth_take. have ltszs := leq_ltn_trans leszi leis. rewrite nth_cat (minn_idPr (ltnW ltszs)). rewrite subnBA // subnK // size_drop ltn_subLR //. have:= ltnW ltszs; rewrite -ltnS => /ltnW; rewrite -subn_eq0 => /eqP ->. rewrite addn0 (leq_gtF leszi) nth_nseq subn0. rewrite ltn_subRL subnKC // leis. by rewrite nth_default. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition