proposition: Lemma size_incr_first_n sh n : size sh <= n -> size (incr_first_n sh n) = n.
proof: Proof. elim: sh n => [| s0 sh IHsh] /= n; first by rewrite size_nseq. by case: n => //= n; rewrite /= ltnS => /IHsh ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype