proposition: Lemma startrem_accP acc sh nbox pos : is_part sh -> let (start, rem) := startrem acc sh nbox pos in 0 < rem -> (start == acc) || (nth 0 sh (start - acc) + rem <= nth 0 sh (start - acc).-1).
proof: Proof. elim: pos sh => [|p IHpos] [|s0 s] in acc *; rewrite /= ?sub0n ?addn0 ?eqxx //. rewrite subn_gt0 => _ /ltnW; rewrite -subn_eq0 => /eqP ->. by rewrite addn0 eqxx. move=> /andP[Hhead Hpart]. move/(_ s acc.+1 Hpart): IHpos => /=. have:= startrem_acc_geq acc.+1 s nbox p. have:= startrem_accE acc.+1 s nbox p. case: startrem => [start rem]/= Heq Hstart Hrec. case (ltnP 0 rem) => [Hok | {Heq Hrec}]. move/(_ Hok): Hrec => /orP[/eqP eqstart | Hleq {Heq}]/=. case: (leqP (s0 + _) _) => [_ | Hlt _]; first by rewrite eqxx. apply/orP; right; rewrite eqstart subSn // subnn /=. rewrite eqstart subnn addn0 in Heq. by move: Hlt; rewrite -{}Heq addnS ltnS addnAC leq_add2r. case: (leqP (s0 + _) _) => [_ | _ _]; first by rewrite eqxx. apply/orP; right. move: Hstart Hleq; rewrite subnS. rewrite -subn_gt0 => []; case: (start - acc) => //= [[|n]] //= _. by move/leq_trans; apply; case: s Hhead Hpart. rewrite leqn0 => /eqP ->. case: (leqP (s0 + _) _) => [_ | _ _]; first by rewrite eqxx. rewrite addn0; apply/orP; right. move: Hstart; rewrite -subn_gt0 => []. case: (start - acc) => // [[|i]] _ /=; first by case: s Hhead {Hpart}. by move/is_partP: Hpart => [_]; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition