proposition: Lemma included_incr_nth sh i : included sh (incr_nth sh i).
proof: Proof. apply/includedP; split. - rewrite size_incr_nth; case ltnP => Hi //=. exact: (leq_trans Hi). - move=> j; rewrite nth_incr_nth. exact: leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype