proposition: Lemma isantisym_alt (p : {mpoly R[n]}) : p != 0 -> p \is antisym -> p \is ('C(n, 2)).-homog -> p = p@_(rho) *: 'a_rho.
proof: Proof. Proof using Hchar. move=> Hpn0 Hanti Hhom. apply/eqP; rewrite -subr_eq0; apply contraT => Habs. have /(isantisym_mlead_rho Habs) H : p - p@_(rho) *: 'a_(rho) \is antisym. by apply/(rpredD Hanti)/rpredNr/rpredZ/alt_anti. move: Habs => /mlead_supp. have /H{H} ->: p - p@_(rho) *: 'a_(rho) \is ('C(n, 2)).-homog. by apply/(rpredD Hhom)/rpredNr/rpredZ/alt_homog. rewrite mcoeff_msupp linearB /= linearZ linear_sum /=. rewrite (bigID (xpred1 1%g)) /= big_pred1_eq. rewrite odd_perm1 /= expr0 scale1r msym1m mcoeffX eq_refl /=. rewrite big1; first by rewrite addr0 mulr1 subrr eq_refl. move=> s Hs; apply /eqP; move: Hs; apply contraR. rewrite linearZ /= msymX mcoeffX. case: ( _ =P rho); last by rewrite mulr0 eq_refl. rewrite mnmP => H _; rewrite -eq_invg1; apply/eqP. rewrite -permP => i; rewrite perm1. move/(_ i) : H => /=. rewrite /rho !mnm_tnth !tnth_mktuple !mnm_tnth !tnth_mktuple !subn1 => H. rewrite -[LHS]rev_ordK -[RHS]rev_ordK; congr rev_ord. apply val_inj => /=; rewrite !subnS. have/ltn_predK neq11 := ltn_ord i. by rewrite -[X in (X - _)%N]neq11 -[X in (X - i)%N]neq11 !subSKn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition