proposition: Lemma minus_not_in : forall (A : part_set E) (x : E), ~ in_part x A -> Equal (minus_part A x) A.
proof: Proof. simpl in |- *. unfold eq_part, minus_part, diff, single in |- *; simpl in |- *. intro A. case A; unfold pred_compatible in |- *; simpl in |- *. intros a pa x neg_a_x x0. generalize (pa x0 x). intuition auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop