proposition: Lemma add_part_com : forall (A : part_set E) (x y : E), Equal (add_part (add_part A x) y) (add_part (add_part A y) x).
proof: Proof. unfold add_part in |- *. intros. apply Trans with (union A (union (single x) (single y))); auto with algebra. apply Trans with (union A (union (single y) (single x))); auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop