proposition: Lemma filter2CE (ltT : rel A) (p : pred A) f t1 t2 : irreflexive ltT -> antisymmetric ltT -> transitive ltT -> {in f &, total (fun k t => (k == t) || ltT k t)} -> {in p, forall z, ltT z t2 = (z == t1) || ltT z t1} -> uniq f -> p t1 -> t1 \in f -> filter (ltT^~ t2) (filter p (sort (fun k t => (k == t) || ltT k t) f)) = filter (ltT^~ t1) (filter p (sort (fun k t => (k == t) || ltT k t) f)) ++ [:: t1].
proof: Proof. move=>I Asym T Tot Z U P F; apply: filterCE (I) (T) _ _ _. - by rewrite (sorted_filter T _ _) //; apply: sort_sorted_in_lt. - by move=>z; rewrite mem_filter=>/andP [Pz _]; apply: Z. by rewrite mem_filter mem_sort P F. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)