proposition: Lemma filter_flat_map : forall {A B} g (f: B -> bool) xs, filter f (flat_map g xs) = flat_map (fun x : A => filter f (g x)) xs.
proof: Proof. intros; rewrite !flat_map_flatten. rewrite flatten_filter, map_map; reflexivity. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith