proposition: Lemma map_filter {A B} f (g : A -> B) l : filter f (map g l) = map g (filter (fun b => f (g b)) l).
proof: Proof. induction l; auto. simpl. destruct (f (g a)); auto. simpl. congruence. Qed.
imports: Arith ZArith String List Psatz Factorial