proposition: Lemma sym_smalln : n <= 1 -> (@symmetric n R) =i predT.
proof: Proof. Proof using. move=> Hn p /=; rewrite [RHS]unfold_in /=. apply/issymP => s. by rewrite (perm_smalln Hn s) msym1m. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition