proposition: Lemma filter_sub {A} f g l : (forall x : A, f x = true -> g x = true) -> filter f l = filter g (filter f l).
proof: Proof. intros H. induction l; simpl; auto. rewrite IHl. destruct (f a) eqn:E. - simpl. rewrite H; auto. congruence. - congruence. Qed.
imports: Arith ZArith String List Psatz Factorial