proposition: Lemma nth_add_ribbon_start : nth 0 res start = nth 0 sh start + rem.
proof: Proof. rewrite /add_ribbon_on nth_cat size_take. by rewrite -/(minn _ _) (minn_idPl lessz) ltnn subnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition