fact: Definition add_ribbon_on sh start stop rem := (take start sh) ++ (nth 0 sh start + rem :: map S (drop start (take stop sh))) ++ drop stop.+1 sh ++ nseq (stop - size sh) 1.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition