proposition: Lemma eq_inv_catr (u1 v1 : seq S) (u2 v2 : seq T) : eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> eq_inv v1 v2.
proof: Proof. move/eq_invP => []; rewrite !size_cat => Hsz Hinv Hszu. apply/eq_invP; split. by apply/eqP; rewrite -(eqn_add2l (size u1)) {2}Hszu Hsz. move=> i j /andP[Hij Hj]. have /Hinv : size u1 + i <= size u1 + j < size u1 + size v1. by rewrite leq_add2l ltn_add2l Hij /=; apply: (leq_trans Hj). by rewrite !nth_cat -Hszu !ltnNge !leq_addr /= !addKn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp