proposition: Lemma startrem_acc_geq acc sh nbox pos : acc <= (startrem acc sh nbox pos).1.
proof: Proof. elim: pos sh acc => [|p IHpos] [|s0 s] acc /=; rewrite ?leqnn ?leq_addr //. case: startrem (IHpos s acc.+1) => [start rem] /= /ltnW Has /=. by case: (leqP (s0 + _) _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition