proposition: Lemma isantisym_tpermP p : reflect (forall i j, msym (tperm i j) p = if (i != j) then - p else p) (p \is antisym).
proof: Proof. Proof using. apply/(iffP forallP) => /= [Hanti i j | Htperm s]. - rewrite (eqP (Hanti (tperm _ _))) odd_tperm. by case: (i != j); rewrite !simplexp. - case: (prod_tpermP s) => ts -> {s} Hall. elim: ts Hall => [_ | t0 ts IHts] /=. by rewrite !big_nil odd_perm1 /= msym1m expr0 scale1r. move=> /andP[H0 {}/IHts/eqP Hrec]. rewrite !big_cons msymMm Htperm H0 msymN Hrec. rewrite odd_mul_tperm H0 /=. 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