proposition: Lemma mecharP k m : mechar k m = [exists h : {set 'I_n}, (m == mesym1 h) && (#|h| == k)].
proof: Proof. apply/idP/existsP=> /=; last first. case=> h /andP[/eqP-> /eqP<-]; rewrite /mechar. rewrite mdeg_mesym1 eqxx /=; apply/forallP=> /= i. by rewrite mnmE leq_b1. case/andP=> /eqP<- /forallP /= mE; exists [set i | m i != 0%N]. apply/andP; split; [apply/eqP/mnmP=> i|apply/eqP]. by rewrite mnmE inE; have := mE i; case: (m i)=> [|[|]]. rewrite mdegE (bigID (fun i => m i == 0%N)) /=. rewrite big1 ?add0n; last by move=> i /eqP->. rewrite (eq_bigr (fun _ => 1%N)) ?sum1_card ?cardsE //. by move=> i; have := mE i; case: (m i) => [|[|]]. 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