proposition: Lemma in_diff : forall (A B : part_set E) (x : E), in_part x A -> ~ in_part x B -> in_part x (diff A B).
proof: Proof. intros A B. case A; case B; simpl in |- *. intros a pa b pb. unfold eq_part in |- *; simpl in |- *. intuition. Qed.
imports: Fpart Inter Arith