proposition: Lemma sym_antiE q : (q \is symmetric) = (p * q \is antisym).
proof: Proof. Proof using Hpanti Hpn0. case: (leqP n 1) => Hn; first by rewrite !(sym_smalln Hn) !(antisym_smalln Hn). apply/idP/idP; first exact: sym_anti Hpanti. move: Hpanti => /isantisymP Hsym /isantisymP Hpq. apply/issymP => s. have:= Hpq s; rewrite msymM Hsym => H; apply (mulfI Hpn0). move: H; case: (odd_perm s); rewrite !simplexp //. by move/oppr_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition