proposition: Lemma list_before_filter (f : A -> bool) l x y : list_before l x y -> f x -> f y -> list_before (filter f l) x y.
proof: Proof. unfold list_before; ins; desf; splits; eauto with hahn. repeat (rewrite filter_app; ins); desf; eauto. Qed.
imports: Arith HahnBase HahnList HahnRelationsBasic