proposition: Lemma monotoneFilter: forall {A: Type} (f: A -> bool), monotoneSetFn (filter f).
proof: Proof. intros. unfolds_base. introv Hs Hin. apply FilterLIn. apply FilterLIn in Hin. repnd. dands; cpx. Qed.
imports: UsefulTypes bin_rels Omega