proposition: Lemma startrem0P acc sh nbox pos : nth 0 sh 0 + pos <= nth 0 sh pos + nbox -> startrem acc sh nbox pos = (acc, nth 0 sh pos + nbox - (nth 0 sh 0 + pos)).
proof: Proof. case: sh pos => [|s0 sh] [|pos]//=; nat_norm => //. - by rewrite -subn_eq0 => /eqP ->; rewrite addn0. - by rewrite subn0 addKn. - by move=> ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition