proposition: Lemma not_in_part_trans : forall (x : E) (A B : part_set E), ~ in_part x A -> Equal A B -> ~ in_part x B.
proof: Proof. unfold in_part in |- *. intros x A B. case A; case B; simpl in |- *. intros a pa b pb. unfold eq_part in |- *; simpl in |- *. intuition. elim (H0 x); auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop