proposition: Lemma tcast_take_inj n m k (H : minn n k = m) (nk : n = k) (t v : k.-tuple A) : tcast H [tuple of take n t] = tcast H [tuple of take n v] -> t = v.
proof: Proof. subst m n => /=. case => /= tv. apply eq_from_tnth => i. rewrite (tnth_nth t!_i) [in X in _ = X](tnth_nth t!_i). by rewrite -(@nth_take k) // -[in X in _ = X](@nth_take k) // tv. Qed.
imports: mathcomp(all_ssreflect fingroup perm)