proposition: Lemma tnth_uniq (T : eqType) n (t : n.-tuple T) (i j : 'I_n) : uniq t -> (t !_ i == t !_ j) = (i == j).
proof: Proof. pose a := t !_ i; rewrite 2!(tnth_nth a) => *. by rewrite nth_uniq // size_tuple. Qed.
imports: mathcomp(all_ssreflect fingroup perm)