proposition: Lemma startrem_leq_pos sh nbox pos : (startrem 0 sh nbox pos).1 <= pos.
proof: Proof. rewrite -{2}(addn0 pos). elim: pos sh (0) => [|p IHpos] [|s0 s] acc /=; rewrite /= ?addn0 ?add0n //. by rewrite addnC leq_add2r leq_subr. case: startrem (IHpos s acc.+1) => [start rem] /=. case: (leqP (s0 + _) _) => [_ _ | H] /=; first by rewrite leq_addl. by rewrite addSnnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition