proposition: Lemma add_part_comp : forall (A A' : part_set E) (x x' : E), Equal A A' -> Equal x x' -> Equal (add_part A x) (add_part A' x').
proof: Proof. unfold add_part in |- *; auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop