proposition: Lemma filter_filter {A} (f g : A -> bool) l : filter f (filter g l) = filter (fun b => andb (g b) (f b)) l.
proof: Proof. induction l; auto. simpl. unfold andb. destruct (g a); simpl; destruct (f a); simpl; auto. rewrite IHl. auto. Qed.
imports: Arith ZArith String List Psatz Factorial