proposition: Lemma inter_not_in : forall (A B : part_set E) (x : E), ~ in_part x A -> ~ in_part x (inter A B).
proof: Proof. unfold not in |- *; intros. apply H. apply in_part_inter_l with B; auto with *. Qed.
imports: Fpart Inter Arith