proposition: Lemma antisym_submod_closed : submod_closed antisym.
proof: Proof. Proof using. split=> [|c p q /isantisymP sp /isantisymP sq]; apply/isantisymP=> s. by rewrite msym0 scaler0. rewrite msymD msymZ sp sq. by rewrite scalerA commr_sign -scalerA scalerDr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition