proposition: Lemma partition_snd {elt} f (m:t elt) : snd (partition f m) = filter (fun k e => negb (f k e)) m.
proof: Proof. induction m; simpl; auto. rewrite <- IHm. now destruct (partition f m), a, f. Qed.
imports: Coq(EqualitiesFacts)