proposition: Lemma add_part_in_el_diff : forall (A : part_set E) (x y : E), in_part y (add_part A x) -> ~ Equal y x -> in_part y A.
proof: Proof. simpl in |- *. unfold eq_part, add_part, union, single in |- *; simpl in |- *. intro. case A; simpl in |- *. intros a pa. intuition. Qed.
imports: Union Singleton Diff Classical_Prop