fact: Parameter partition : forall (P : E.t -> Prop) (Pdec : forall x : E.t, {P x} + {~ P x}) (s : t), {partition : t * t | let (s1, s2) := partition in compat_P E.eq P -> For_all P s1 /\ For_all (fun x => ~ P x) s2 /\ (forall x : E.t, In x s <-> In x s1 \/ In x s2)}.
imports: Bool OrderedType DecidableType