proposition: Lemma partition_as_filter f (l : list A) : partition f l = (filter f l, filter (fun x => negb (f x)) l).
proof: Proof. induction l as [|x l IH]. - reflexivity. - cbn. rewrite IH. destruct (f x); reflexivity. Qed.
imports: PeanoNat