proposition: Fact leperm_trans : transitive leperm.
proof: Proof. move=> t s u /lepermP[/= st ->{t} Hsst] /lepermP[/= stu ->{u} Hstu]. apply/lepermP; exists (st * stu); first by rewrite mulgA. rewrite Hstu Hsst -addnA; congr (_ + _). by rewrite {}Hsst in Hstu; rewrite (lengthKR Hstu). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype