proposition: Lemma sorted_enum : sorted le_rank (enum X).
proof: Proof. rewrite /sorted. move HX : (enum X) => Alst. destruct Alst => //. apply/(pathP s) => i Hi. rewrite /le_rank -HX. destruct Alst => //. have iA : i < #|X| by rewrite cardE HX (ltn_trans Hi). rewrite -(@enum_val_nth X (xpredT) s (Ordinal iA)). have i1A : i.+1 < #|X| by rewrite cardE HX (leq_ltn_trans Hi). have -> : (nth s (s0 :: Alst) i) = (nth s (enum X) i.+1) by rewrite /= HX. by rewrite -(@enum_val_nth X (xpredT) s (Ordinal i1A)) 2!enum_valK leqnSn. Qed.
imports: mathcomp(all_ssreflect fingroup perm)