proposition: Lemma incr_first_n_nthC sh i j : incr_first_n (incr_nth sh i) j = incr_nth (incr_first_n sh j) i.
proof: Proof. elim: sh i j => [| s0 sh IHsh]. elim=> [| i IHi] [|j] //=. by move/(_ j) : IHi => /= <-; case: i. case=> [| i] [| j] //=. by rewrite IHsh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype