proposition: Lemma filter_sort_in T (P : {pred T}) (leT : rel T) : {in P &, total leT} -> {in P & &, transitive leT} -> forall p s, all P s -> filter p (sort leT s) = sort leT (filter p s).
proof: Proof. move=> /in2_sig leT_total /in3_sig leT_tr p _ /all_sigP[s ->]. by rewrite !(sort_map, filter_map) filter_sort. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)