proposition: Lemma sepitP x s (f : A -> Pred U) : uniq s -> sepit s f =p if x \in s then f x # sepit (filter (predC1 x) s) f else sepit s f.
proof: Proof. case E: (x \in s)=>//. elim: s E=>[|y s IH] //= /[swap]; case/andP=>Hy Hu; rewrite sepit_cons inE; case/orP. - by move/eqP=>->; rewrite eq_refl filter_predC1. move=>Hx h0. have ->: (y != x) by apply/eqP=>Hxy; rewrite Hxy Hx in Hy. by split; case=>ha[h1][{h0}-> Ha]; [rewrite (IH Hx Hu) | rewrite sepit_cons]; case=>hb[h][{h1}-> Hb H]; rewrite joinCA; exists hb, (ha \+ h); split=>//; [rewrite sepit_cons | rewrite (IH Hx Hu)]; exists ha, h. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)