proposition: Lemma invseqE s t1 t2 : invseq s t1 -> invseq s t2 -> t1 = t2.
proof: Proof. move=> Hinv1 Hinv2. have Hsz: size t1 = size t2. by rewrite -(size_invseq Hinv1) -(size_invseq Hinv2). apply: (eq_from_nth (x0 := size s) Hsz) => i Hi1. have:= Hi1; rewrite Hsz => Hi2. have:= Hinv1; rewrite /invseq => /andP[_ Ht1s]. have Hnth1 := linvseq_ltn_szt Ht1s Hi1. rewrite (invseq_nthE Hinv2 Hnth1 Hi2) -Hsz. by move: Ht1s => /linvseqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp