proposition: Lemma union_not_in : forall (A B : part_set E) (x : E), ~ in_part x A -> ~ in_part x B -> ~ in_part x (union A B).
proof: Proof. unfold not in |- *; intros. cut (in_part x A \/ in_part x B). intros H'; try assumption. intuition. auto with *. Qed.
imports: Fpart Inter Arith