proposition: Lemma predi_eltrpE p : i < n -> predi p = predi ('s_i p.1, 's_i p.2).
proof: Proof. Proof using. move=> Hi; apply/idP/idP => [|H]; first exact: predi_eltrp. by rewrite -(eltrpK p) predi_eltrp. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition