proposition: Lemma filter_map_always {A B} f (g : A -> B) l : (forall x, f (g x) = true) -> filter f (map g l) = map g l.
proof: Proof. intros H. induction l as [| a l IHl]. reflexivity. simpl. rewrite H. congruence. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia