proposition: Lemma lt_rank_alt x y : lt_rank x y = (enum_rank x < enum_rank y).
proof: Proof. rewrite /lt_rank /le_rank ltn_neqAle andbC; apply andb_id2r => _. case/boolP : (x == y) => [/eqP ->|xy]; first by rewrite eqxx. apply/esym => /=; apply: contra xy => /eqP H. by apply/eqP/enum_rank_inj/ord_inj. Qed.
imports: mathcomp(all_ssreflect fingroup perm)