proposition: Fact leperm_anti : antisymmetric leperm.
proof: Proof. move=> s t /andP[Hst Hts]; apply: (leperm_lengthE Hst). by apply anti_leq; apply/andP; split; apply leperm_length. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype