proposition: Lemma issym_eltrP n (R : ringType) (p : {mpoly R[n.+1]}) : reflect (forall i, i < n -> msym 's_i p = p) (p \is symmetric).
proof: Proof. apply/(iffP forallP) => /= [Hanti i Hi | Heltr]. - by have /eqP -> := Hanti 's_i. - elim/eltr_ind => [| S i Hi /eqP IH]. + by rewrite msym1m. + by rewrite msymMm (Heltr i Hi) IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition