proposition: Lemma startrem_accE acc sh nbox pos : let (start, rem) := startrem acc sh nbox pos in nth 0 sh (start - acc) + pos + rem = nth 0 sh pos + (start - acc) + nbox.
proof: Proof. elim: pos sh acc => [|p IHpos] [|s0 s] acc /=; rewrite /= ?sub0n ?addn0 ?subnn /= ?add0n ?subn0 ?addn0 //. rewrite addKn nth_nil /= add0n. by rewrite [RHS]addnC -!maxnE maxnC. move/(_ s acc.+1): IHpos. case: startrem (startrem_acc_geq acc.+1 s nbox p) => [start rem] /= Hstart. case: (leqP (s0 + _) _) => [Hle _| Hgt]. by rewrite subnn /= subnKC // addn0 addnC. case: start Hstart => // start /ltnSE Hstart. by rewrite subSS (subSn Hstart) /= !(addnS, addSn) => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition