proposition: Lemma filter_sort T (leT : rel T) : total leT -> transitive leT -> forall p s, filter p (sort leT s) = sort leT (filter p s).
proof: Proof. move=> leT_total leT_tr p s; case Ds: s => // [x s1]. pose leN := relpre (nth x s) leT. pose lt_lex := [rel n m | leN n m && (leN m n ==> (n < m))]. have lt_lex_tr: transitive lt_lex. rewrite /lt_lex /leN => ? ? ? /= /andP [xy xy'] /andP [yz yz']. rewrite (leT_tr _ _ _ xy yz); apply/implyP => zx; move: xy' yz'. by rewrite (leT_tr _ _ _ yz zx) (leT_tr _ _ _ zx xy); apply: ltn_trans. rewrite -{s1}Ds -(mkseq_nth x s) !(filter_map, sort_map); congr map. apply/(@irr_sorted_eq _ lt_lex); rewrite /lt_lex /leN //=. - by move=> ?; rewrite /= ltnn implybF andbN. - exact/sorted_filter/sort_iota_stable. - exact/sort_stable/sorted_filter/iota_ltn_sorted/ltn_trans/ltn_trans. - by move=> ?; rewrite !(mem_filter, mem_sort). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)