proposition: Lemma cat_cancel (xs1 xs2 ys1 ys2 : seq A) (k : A) : k \notin xs1 -> k \notin xs2 -> xs1 ++ k :: ys1 = xs2 ++ k :: ys2 -> (xs1 = xs2) * (ys1 = ys2).
proof: Proof. move=>Nk1 Nk2 E. have Es : size xs1 = size xs2. - have : index k (xs1++k::ys1) = index k (xs2++k::ys2) by rewrite E. by rewrite !index_cat /= (negbTE Nk1) (negbTE Nk2) eqxx !addn0. have Ex : xs1 = take (size xs1) (xs1 ++ k :: ys1). - by rewrite take_cat ltnn subnn /= cats0. rewrite E Es take_cat ltnn subnn /= cats0 in Ex. rewrite {xs1 Nk1 Es}Ex in E *. have : ys1 = drop (size (xs2++[::k])) (xs2++k::ys1). - by rewrite drop_cat size_cat /= addn1 ltnNge ltnW //= subSn // subnn /= drop0. by rewrite E drop_cat size_cat /= addn1 ltnNge ltnW //= subSn // subnn /= drop0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)