proposition: Lemma eq_inv_rembig (u : seq S) (v : seq T) : eq_inv u v -> eq_inv (rembig u) (rembig v).
proof: Proof. move => Hinv; have Heqpos:= eq_inv_posbig Hinv. have:= Hinv; rewrite -!eq_invP => [][Hsz Heq]. rewrite !size_rembig -Hsz; split => //= i j /andP[Hij Hj]. rewrite -!nth_rembig /shift_pos -Heqpos. case (ltnP i (posbig u)) => Hipos; case (ltnP j (posbig u)) => Hjpos; apply: Heq. - rewrite Hij /=; apply: (ltn_trans Hj). by move: Hj; case: (size u). - rewrite (leq_trans Hij (leqnSn _)) /=. suff -> : (size u) = (size u).-1.+1 by rewrite ltnS. by move: Hj; rewrite -ltnS; case: (size u). - by exfalso; have:= leq_trans (leq_trans Hjpos Hipos) Hij; rewrite ltnn. - rewrite ltnS Hij /=. suff -> : (size u) = (size u).-1.+1 by rewrite ltnS. by move: Hj; rewrite -ltnS; case: (size u). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp