proposition: Lemma leperm_maxperm s : s <=R maxperm.
proof: Proof. by rewrite -leperm_maxpermMl -{1}maxpermV mulVg leperm1p. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype