proposition: Lemma alt_anti m : 'a_m \is antisym.
proof: Proof. Proof using. apply/isantisymP => S. rewrite /alternpol (big_morph (msym S) (@msymD _ _ _) (@msym0 _ _ _)). rewrite scaler_sumr. rewrite [RHS](reindex_inj (mulIg S)); apply: eq_big => //= s _. rewrite msymZ -msymMm scalerA; congr (_ *: _). by rewrite odd_permM signr_addb [X in (_ = _ * X)]mulrC signrMK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition