proposition: Lemma perm_smalln : n <= 1 -> forall s : 'S_n, s = 1%g.
proof: Proof. Proof using. by case: n => [|[|//]] _ s; [rewrite (permS0 s) | rewrite (permS1 s)]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition