proposition: Lemma sepit_cat s1 s2 f : sepit (s1 ++ s2) f =p sepit s1 f # sepit s2 f.
proof: Proof. elim: s1 s2=>[|x s1 IH] s2 h /=; split. - case=>hs [E {h}-> H2]. exists Unit, (seqjoin hs); rewrite unitL. by split=>//; [rewrite sepit0 | exists hs]. - by case=>h1[h2][{h}->]; rewrite sepit0=>->; rewrite unitL. - case=>/=; case=>[|h0 hs]; case=>//= /eqP; rewrite eqSS=>/eqP E. rewrite /seqjoin !big_cons /= =>->[H0 HS]. case: (IH s2 (seqjoin hs)).1; first by exists hs. move=>h1[h2][HJ H1 H2]; rewrite /seqjoin in HJ. exists (h0 \+ h1), h2; rewrite HJ joinA; split=>//. by rewrite sepit_cons; exists h0, h1. case=>h1[h2][{h}->[]]; case=>[|h0 hs1]; case=>//= /eqP; rewrite eqSS=>/eqP E1. rewrite /seqjoin !big_cons /= =>{h1}->[H0 H1]; case=>hs2[E2 {h2}-> H2]. exists (h0 :: hs1 ++ hs2); rewrite /seqjoin big_cons big_cat joinA; split=>//=. - by rewrite !size_cat E1 E2. rewrite zip_cat //=; split=>//. by apply/All_cat. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)