fact: Definition lepermP s t : reflect (exists2 u : 'S_n, t = s * u & length t = length s + length u) (s <=R t) := lepermP s t.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype