proposition: Lemma sorted_of_tnth_leq (X : finType) (n : nat) (r : rel X) (t : n.-tuple X) (r_trans : transitive r) (r_refl : reflexive r) (Hx : sorted r t) : forall (l p : 'I_n), l <= p -> r t!_l t!_p.
proof: Proof. move=> l p leqlp. case/boolP : (l == p) => Hcase. - move/eqP in Hcase; rewrite Hcase; apply r_refl. - apply sorted_of_tnth => //; by rewrite ltn_neqAle leqlp Hcase. Qed.
imports: mathcomp(all_ssreflect fingroup perm)