proposition: Lemma filter_app : forall l1 l2 P, filter P (l1 ++ l2) = filter P l1 ++ filter P l2.
proof: Proof. Proof using. intros. unfold filter. assert (forall accu, fold_right (fun x acc => If P x then x::acc else acc) accu (l1 ++ l2) = fold_right (fun x acc => If P x then x::acc else acc) nil l1 ++ fold_right (fun x acc => If P x then x::acc else acc) nil l2 ++ accu). { induction l1; intros. { rew_list. gen accu. induction l2; intros. { auto. } { rew_listx. case_if. rew_list. fequals. rewrite IHl2. fequals. } } { rew_listx. case_if. rew_list. fequals. rewrite IHl1. fequals. } } specializes H (@nil A). rewrite~ app_nil_r in H. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)