proposition: Lemma msymX m s : msym s 'X_[m] = 'X_[m#(s^-1)%g].
proof: Proof. apply/mpolyP=> m'; rewrite mcoeff_sym !mcoeffX. congr (_ : bool)%:R; apply/eqP/eqP=> [->|<-]. + by apply/mnmP=> i; rewrite !mnmE permKV. + by apply/mnmP=> i; rewrite !mnmE permK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg