proposition: Lemma filterCE (ltT : rel A) f t1 t2 : irreflexive ltT -> transitive ltT -> sorted ltT f -> {in f, forall z, ltT z t2 = (z == t1) || ltT z t1} -> t1 \in f -> filter (ltT^~ t2) f = filter (ltT^~ t1) f ++ [:: t1].
proof: Proof. move=>I T S Z F; have U : uniq f by apply: sorted_uniq T I _ S. rewrite -(filter_pred1_uniq U F); apply: irr_sorted_eq (T) I _ _ _ _ _. - by apply: sorted_filter T _ _ S. - rewrite -[filter (ltT^~ t1) _]revK -[filter (pred1 t1) _]revK -rev_cat. rewrite rev_sorted -filter_rev filter_pred1_uniq ?(mem_rev,rev_uniq) //. rewrite /= path_min_sorted ?(rev_sorted, sorted_filter T _ S) //. by apply/allP=>x; rewrite mem_rev mem_filter=>/andP []. move=>x; rewrite mem_cat !mem_filter /=. case X: (x \in f); last by rewrite !andbF. by rewrite Z // orbC !andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)