proposition: Lemma issym_tpermP p : reflect (forall i j, msym (tperm i j) p = p) (p \is symmetric).
proof: Proof. Proof using. apply/(iffP forallP) => /= [Hsym i j | Htperm s]. - by rewrite (eqP (Hsym (tperm _ _))). - case: (prod_tpermP s) => ts -> {s} Hall. elim: ts Hall => [_ | t0 ts IHts] /=. by rewrite !big_nil /= msym1m. move=> /andP[_ {}/IHts/eqP Hrec]. by rewrite !big_cons msymMm Htperm Hrec. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition