proposition: Lemma startrem_leq_size sh nbox pos : let (start, rem) := startrem 0 sh nbox pos in 0 < rem -> start <= size sh.
proof: Proof. rewrite -(addn0 (size sh)). elim: pos sh {1 3}(0) => [|p IHpos] [|s0 s] acc /=; rewrite /= ?addn0 ?add0n ?leq_addl//. move=> /(leq_ltn_trans (leq0n _)). rewrite subn_gt0 => /ltnW; rewrite -subn_eq0 => /eqP ->. by rewrite addn0. 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