proposition: Lemma nth_incr_first_n sh n i : nth 0 (incr_first_n sh n) i = if i < n then (nth 0 sh i).+1 else nth 0 sh i.
proof: Proof. elim: sh n i => [| s0 s IHs] n i /=. by rewrite nth_nseq nth_default. case: n i => [| n] //= [| i] //=. exact: IHs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype