proposition: Lemma included_incr_nth_inner inner outer i : nth 0 inner i < nth 0 outer i -> included inner outer -> included (incr_nth inner i) outer.
proof: Proof. move=> Hnth /includedP[Hsize Hincl]. apply/includedP; split. - rewrite size_incr_nth; case ltnP => _; first exact Hsize. rewrite ltnNge; apply/negP => Hout. by move: Hnth; rewrite (nth_default _ Hout). - move=> j; rewrite nth_incr_nth. by case eqP => [<- | _]; rewrite ?add1n ?add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype