proposition: Lemma minus_part_com : forall (A : part_set E) (x y : E), Equal (minus_part (minus_part A x) y) (minus_part (minus_part A y) x).
proof: Proof. unfold minus_part in |- *. intros. simpl in |- *. unfold eq_part, diff, single in |- *; simpl in |- *. intro. intuition. Qed.
imports: Union Singleton Diff Classical_Prop