proposition: Lemma partition_aux_spec f m acc1 acc2 : partition_aux f m acc1 acc2 = (filter_aux f m acc1, filter_aux (fun k e => negb (f k e)) m acc2).
proof: Proof. revert acc1 acc2. induction m as [ | c l Hl x e r Hr ]; simpl. - trivial. - intros acc1 acc2. destruct (f x e); simpl; now rewrite Hr, Hl. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)