proposition: Lemma pperm_cat_consR s1 s2 t1 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 /H; apply. apply: perm_ind; last 1 first. - move=>s2 s1 s3 H1 IH1 H2 IH2 x r1 t1 r2 t2 E1 E2. case: (@In_split _ x s2). - by apply: pperm_in H1 _; rewrite E1 Mem_cat; right; left. move=>s4 [s5] E; apply: (@pperm_trans (s4++s5)); first by apply: IH1 E1 E. by apply: IH2 E E2. - by move=>x []. - move=>x t1 t2 H IH y [|b s1] s2 [|c p1] p2 /= [E1 E2] [E3 E4]; subst x; rewrite ?E1 ?E2 ?E3 ?E4 in H * =>//. - by subst y; apply: pperm_trans H _. - by apply: pperm_trans H. by apply: permutation_skip=>//; apply: IH E2 E4. move=>x y p1 p2 H IH z [|b s1] t1 [|c s2] t2 /= [E1 E2] [E3 E4]; subst x y; rewrite -?E2 -?E4 in H IH * =>//. - by apply: permutation_skip. - case: s2 E4=>/=[|a s2][<-]=>[|E4]; apply: permutation_skip=>//. by subst p2; apply: pperm_trans H _; apply pperm_cons_catAC. - case: s1 E2=>/=[|a s1][<-]=>[|E2]; apply: permutation_skip=>//. by subst p1; apply: pperm_trans H; apply pperm_cons_catCA. case: s1 E2=>/=[|a s1][->]=>E2; case: s2 E4=>/=[|d s2][->]=>E4; rewrite ?E2 ?E4 in H IH *. - by apply: permutation_skip. - apply: (@pperm_trans [:: d, z & s2 ++ t2]); last by apply: permutation_swap. by apply: permutation_skip=>//; apply/(pperm_trans H _ )/pperm_cons_catAC. - apply: (@pperm_trans [:: a, z & s1 ++ t1]); first by apply: permutation_swap. by apply: permutation_skip=>//; apply/pperm_trans/H/pperm_cons_catCA. by apply: permutation_swap; apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)