proposition: Lemma partition_alt f m : partition f m = (filter f m, filter (fun k e => negb (f k e)) m).
proof: Proof. unfold partition, filter. now rewrite partition_aux_spec. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)