proposition: Lemma anti_anti p q : p \is antisym -> q \is antisym -> p * q \is symmetric.
proof: Proof. Proof using. move=> /isantisymP Hp /isantisymP Hq. apply/issymP => s; rewrite msymM Hp Hq. 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