proposition: Lemma leperm_maxpermMl s t : (maxperm * t <=R maxperm * s) = (s <=R t).
proof: Proof. suffices {s t} impl u v : u <=R v -> maxperm * v <=R maxperm * u. apply/idP/idP; last exact: impl. rewrite -{2}(mulKg maxperm s) -{2}(mulKg maxperm t) maxpermV. exact: impl. move/lepermP => /= [s ->{v} Hlen]. apply/lepermP; exists s^-1; first by rewrite -!mulgA mulgV mulg1. rewrite !length_maxpermMl Hlen lengthV subnDA subnK //. by rewrite -(leq_add2l (length u)) -Hlen subnKC length_max. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype