proposition: Lemma invseq_nthE s t : invseq s t -> forall i j, i < size s -> j < size t -> (i = nth (size s) t j <-> nth (size t) s i = j).
proof: Proof. move=> Hinv i j Hi Hj. move: Hinv; rewrite /invseq => /andP[/linvseqP Hst /linvseqP Hts]. split => H. + by move/(_ j Hj) : Hts; rewrite H. + by move/(_ i Hi) : Hst; rewrite H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp