proposition: Fact leperm_lengthE s t : s <=R t -> length s = length t -> s = t.
proof: Proof. move/lepermP => /= [u -> ->] /eqP. rewrite -{1}(addn0 (length s)) eqn_add2l eq_sym => /eqP/length_eq0 ->. by rewrite mulg1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype