proposition: Lemma not_in_part_trans_eq : forall (x y : E) (A : part_set E), ~ in_part x A -> Equal x y -> ~ in_part y A.
proof: Proof. unfold in_part in |- *. intros x y A. case A; intros a pa. simpl in |- *. intuition. apply H. apply (pa y x); auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop