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