proposition: Fact lepermP s t : reflect (exists2 u, t = s * u & length t = length s + length u) (s <=R t).
proof: Proof. apply (iffP existsP) => [] /= [u]. - by move=> /andP[/eqP Heq /eqP Hlen]; exists u. - by move=> /eqP Heq /eqP Hlen; exists u; apply/andP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype