proposition: Lemma eq_inv_transp d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (u v : seq S) a b (U V : seq T) A B : (a < b)%O -> (A < B)%O -> size u = size U -> eq_inv (u ++ [:: a; b] ++ v) (U ++ [:: A; B] ++ V) -> eq_inv (u ++ [:: b; a] ++ v) (U ++ [:: B; A] ++ V).
proof: Proof. move=> Hab HAB HuU /eq_invP[Hsz Hinv]. apply/eq_invP; split; first by move: Hsz; rewrite !size_cat /=. have Hsztransp : (size (u ++ [:: a, b & v])) = (size (u ++ [:: b, a & v])) by rewrite !size_cat. move=> i j /andP[Hij Hj]. case/altP: (i =P (size u)) => Hiu. - subst i; rewrite {2}HuU !nth_sizeu. case/altP: (j =P (size u)) => Hju. + by subst j; rewrite {2}HuU !nth_sizeu !lexx. case/altP: (j =P (size u).+1) => Hju1. + subst j; rewrite {2}HuU !nth_sizeu1. by rewrite !leNgt Hab HAB. + move/(_ (size u).+1 j) : Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinv. have {Hyp} {}/Hinv : Hyp. by rewrite /Hyp ltn_neqAle eq_sym Hju Hij; move: Hj; rewrite !size_cat. rewrite (nth_transp _ _ _ Hju Hju1). rewrite HuU in Hju; rewrite HuU in Hju1. rewrite (nth_transp _ _ _ Hju Hju1). by rewrite {2}HuU !nth_sizeu1. case/altP: (i =P (size u).+1) => Hiu1. - subst i; rewrite {2}HuU !nth_sizeu1. case/altP: (j =P (size u).+1) => Hju1. + subst j; rewrite {2}HuU !nth_sizeu1. by rewrite !lexx. + move/(_ (size u) j) : Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinv. have {Hyp}/Hinv : Hyp. by rewrite /Hyp (ltnW Hij) /=; move: Hj; rewrite !size_cat. have Hju : j != size u by rewrite eq_sym (ltn_eqF Hij). rewrite (nth_transp _ _ _ Hju Hju1). rewrite HuU in Hju; rewrite HuU in Hju1. rewrite (nth_transp _ _ _ Hju Hju1). by rewrite {2}HuU !nth_sizeu. - rewrite (nth_transp _ _ _ Hiu Hiu1). rewrite HuU in Hiu; rewrite HuU in Hiu1. rewrite (nth_transp _ _ _ Hiu Hiu1). rewrite -HuU in Hiu; rewrite -HuU in Hiu1. case/altP: (j =P (size u)) => Hju. + subst j; rewrite {2}HuU !nth_sizeu. move/(_ i (size u).+1) : Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinv. have {Hyp}/Hinv : Hyp. rewrite /Hyp (leq_trans Hij (leqnSn _)) /=; rewrite !size_cat /=. by rewrite !addnS !ltnS; exact: leq_addr. by rewrite {2}HuU !nth_sizeu1. case/altP: (j =P (size u).+1) => Hju1. + subst j; rewrite {2}HuU !nth_sizeu1. move/(_ i (size u)) : Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinv. have {Hyp}/Hinv : Hyp. rewrite /Hyp -ltnS ltn_neqAle Hiu1 Hij /=. by rewrite -[size u]addn0 size_cat ltn_add2l. by rewrite {2}HuU !nth_sizeu. + rewrite (nth_transp _ _ _ Hju Hju1). rewrite HuU in Hju; rewrite HuU in Hju1. rewrite (nth_transp _ _ _ Hju Hju1). move/(_ i j) : Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinv. have {Hyp}/Hinv : Hyp. by rewrite /Hyp Hij /=; move: Hj; rewrite !size_cat. by apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp