proposition: Lemma included_decr_nth u i : included (decr_nth u i) u.
proof: Proof. elim: u i => [| u0 u IHu] [| i] //=. case: u0 => [| [| u0]] //=. by rewrite ltnS (leqnSn u0) (included_refl u). by rewrite (leqnn u0) (IHu i). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype