proposition: Lemma partition_filter_eq {A} : forall (f : A -> bool) l, fst (List.partition f l) = List.filter f l.
proof: Proof. induction l; simpl; eauto. destruct (List.partition f l); destruct (f a); simpl in *; congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts