proposition: Lemma nth_add_ribbon_stop_lt i : stop < i -> nth 0 res i = nth 0 sh i.
proof: Proof. move=> ltsi. rewrite /add_ribbon_on nth_cat size_take. have ltszs := leq_ltn_trans less ltsi. rewrite -/(minn _ _) (minn_idPl lessz) (leq_gtF (ltnW ltszs)). rewrite nth_cat /= size_map sztd ltnS. rewrite leq_subLR subnKC //. rewrite leq_min (ltn_geF ltsi) //=. rewrite nth_cat size_drop -(subSn lesmin) subnBA; last exact: ltnW. rewrite (subnK (ltnW ltszs)) /minn. case: (ltnP stop (size sh)) => [ltstsz | leszst]. rewrite ltn_subRL subnKC //. have := ltnW ltstsz; rewrite -subn_eq0 => /eqP -> /=. rewrite nth_nil nth_drop subnKC //. by case: ltnP => // /(nth_default 0) ->. have:=leszst; rewrite -ltnS => /ltnW; rewrite -subn_eq0 => /eqP -> /=. rewrite subn0 nth_nseq. case: i ltsi {ltszs} => // j /ltnSE ltsj. rewrite subSS ltn_subRL (subnKC (leq_trans leszst ltsj)). rewrite (leq_gtF ltsj) nth_default //. by apply/ltnW; rewrite ltnS (leq_trans leszst ltsj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition