proposition: Lemma startrem_leq sh nbox pos : let (start, rem) := startrem 0 sh nbox pos in 0 < rem -> start <= minn pos (size sh).
proof: Proof. move: (startrem_leq_pos sh nbox pos) (startrem_leq_size sh nbox pos). case: startrem => [start rem]// lespos /[apply]. by rewrite leq_min {}lespos => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition