proposition: Lemma le_lt_rank_trans u v w : le_rank u v -> lt_rank v w -> lt_rank u w.
proof: Proof. rewrite /lt_rank => uv /andP[vw H]. rewrite (le_rank_trans uv vw) /=; apply: contra H => /eqP ?. subst w. by rewrite (@le_rank_asym u v) // uv. Qed.
imports: mathcomp(all_ssreflect fingroup perm)