proposition: Lemma sorted_of_tnth {C : eqType} (r : rel C) k (t : k.-tuple C) : transitive r -> sorted r t -> forall a b : 'I_k, a < b -> r (t !_ a) (t !_ b).
proof: Proof. move=> r_trans r_sorted a b ab. rewrite (tnth_nth t!_b) {2}(tnth_nth t!_b). apply sorted_of_nth => //; by rewrite ab size_tuple /=. Qed.
imports: mathcomp(all_ssreflect fingroup perm)