proposition: Lemma diff_in_r : forall (A B : part_set E) (x : E), in_part x (diff A B) -> ~ in_part x 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