proposition: Lemma minus_part_not_in : forall (A : part_set E) (x : E), ~ in_part x (minus_part A x).
proof: Proof. simpl in |- *. intro. case A; simpl in |- *. intros a pa. intuition. Qed.
imports: Union Singleton Diff Classical_Prop