proposition: Lemma inter_add_part_not_in : forall (A B0 B : part_set E) (x : E), ~ in_part x B0 -> Equal A (add_part B0 x) -> ~ in_part x B -> Equal (inter B0 B) (inter A B).
proof: Proof. unfold add_part in |- *. intros A B0 B x H' H'0 H'1; try assumption. apply Trans with (inter (union B0 (single x)) B). auto with *. apply Trans with (union (inter B0 B) (inter (single x) B)). apply Trans with (union (inter B0 B) (empty E)). auto with *. apply union_comp; auto with *. apply Sym. apply in_eq_part. intros x0 H'2; try assumption. cut (Equal x x0). intros H'3; try assumption. absurd (in_part x0 B). unfold not in |- *; intro. unfold not in H'1. apply H'1. apply in_part_trans_eq with x0; auto with *. apply in_part_inter_r with (single x). auto with *. cut (in_part x0 (single x)). auto with *. apply in_part_inter_l with B. auto with *. intros x0 H'2; try assumption. absurd (in_part x0 (empty E)); auto with *. auto with *. auto with *. Qed.
imports: Fpart Inter Arith