proposition: Lemma antisym_char2 : (2 \in [char R]) -> symmetric =i antisym.
proof: Proof. Proof using. move=> Hchar p /=; apply/issymP/isantisymP => H s; by rewrite H oppr_char2; first rewrite expr1n scale1r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition