proposition: Lemma leperm1p s : (1%g : 'S_n) <=R s.
proof: Proof. apply/lepermP; exists s; first by rewrite mul1g. by rewrite length1 add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype