proposition: Lemma filter_app {A} f (l1 l2 : list A) : filter f (l1 ++ l2) = filter f l1 ++ filter f l2.
proof: Proof. induction l1 as [| a l IHl]; simpl. reflexivity. destruct (f a); simpl; congruence. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia