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