fact: Definition leperm_lengthE : forall s t, s <=R t -> length s = length t -> s = t := leperm_lengthE.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype