proposition: Lemma perm_cat_consR s1 t1 s2 t2 x : perm (s1 ++ x :: t1) (s2 ++ x :: t2) -> perm (s1 ++ t1) (s2 ++ t2).
proof: Proof. move: s1 t1 s2 t2 x. suff H: forall r1 r2, perm r1 r2 -> forall x s1 t1 s2 t2, r1 = s1 ++ x :: t1 -> r2 = s2 ++ x :: t2 -> perm (s1 ++ t1) (s2 ++ t2). - by move=>s1 t1 s2 t2 x; move/H; apply. apply: perm_ind2; last 1 first. - move=>s2 s1 s3 H1 IH1 H2 IH2 x r1 t1 r2 t2 E1 E2. case: (@in_split x s2). - apply: perm_in H1 _; rewrite E1; apply: (@perm_in (x::r1++t1))=>//. by rewrite InE; left. move=>s4 [s5] E; apply: (@perm_trans (s4++s5)); first by apply: IH1 E1 E. by apply: IH2 E E2. - by move=>x []. - move=>x t1 t2 H IH y s1 s2 p1 p2 E1 E2. case: s1 E1=>[|b s1] /=; case: p1 E2=>[|c p1] /= E1 E2. - by case: E1 E2=><- <- [<-]. - apply: (@perm_trans (p1 ++ c :: p2))=>//. by case: E1 H=><- ->; case: E2=><- ->. - case: E1 E2 H=><- <- [<-] ->; apply: (@perm_trans (s1 ++ x:: s2)). by apply: perm_cons_cat_consL. case: E1 E2 H IH=><- -> [<-] -> H IH. apply: permutation_skip eq_refl eq_refl _=>//; apply: IH eq_refl eq_refl. move=>x y p1 p2 H IH z s1 t1 s2 t2 E1 E2. case: s1 E1 H IH=>[|b s1]; case: s2 E2=>[|c s2]=>/=. - case=><- <- [<-] <- H IH; apply: permutation_skip eq_refl eq_refl H. - case=><-; case: s2=>[|b s2] /=. - by case=><- <-; case=><- H IH; apply: permutation_skip eq_refl H. case=><- -> [<-] <- H IH. by apply: permutation_skip eq_refl eq_refl _=>//; apply: perm_trans H _. - case=><- <- [<-]; case: s1=>[|a s1] /=. - by case=><- H IH; apply: permutation_skip eq_refl eq_refl _. by case=><- -> H IH; apply: permutation_skip eq_refl eq_refl _=>//; apply: perm_trans H. case=><-; case: s2=>[|a s2] /=; case: s1=>[|d s1] /=. - by case=><- <- [<-] <- <- H IH; apply: permutation_skip eq_refl eq_refl _. - case=><- <- [<-] <- -> H IH. apply: (@perm_trans (x::y::s1 ++ t1)); first by apply: permutation_swap eq_refl. by apply: permutation_skip eq_refl eq_refl _=>//; apply: perm_trans H. - case=><- -> [<-] <- <- H IH. apply: (@perm_trans (y::x::s2++t2)); last by apply: permutation_swap eq_refl. by apply: permutation_skip eq_refl eq_refl _ =>//; apply: perm_trans H _. case=><- -> [<-] <- -> H IH. apply: (@perm_trans (x::y::s1++t1)); first by apply: permutation_swap eq_refl. by apply: permutation_skip eq_refl eq_refl _=>//; apply: permutation_skip eq_refl eq_refl _=>//; apply: IH eq_refl eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)