proposition: Lemma mesymlm_rbound b : (mesymlm n b <= rbound b)%MM.
proof: Proof. Proof using. apply/mnm_lepP => i; rewrite !mnmE inE. case (ssrnat.ltnP i b) => [/= Hb| //]. by rewrite subn_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition