proposition: Lemma partition_spec2' s f : (partition f s)#2 = filter (fun x => negb (f x)) s.
proof: Proof. induction s as [ | h l Hl x r Hr ]; simpl. - trivial. - rewrite <- Hl, <- Hr. now destruct (partition f l), (partition f r), (f x). Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int