proposition: Lemma minus_trans_not_in : forall (A : part_set E) (x y : E), ~ in_part y A -> ~ in_part y (minus_part A x).
proof: Proof. simpl in |- *. unfold eq_part, minus_part, diff, single in |- *; simpl in |- *. intro. case A; simpl in |- *. intros a pa. intuition. Qed.
imports: Union Singleton Diff Classical_Prop