proposition: Lemma startremE sh nbox pos : let (start, rem) := startrem 0 sh nbox pos in nth 0 sh start + pos + rem = nth 0 sh pos + start + nbox.
proof: Proof. case: startrem (startrem_accE 0 sh nbox pos) => start rem. by rewrite subn0; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition