proposition: Lemma inter_add_part : 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 A B) (add_part (inter B0 B) x).
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)). auto with *. apply union_comp; auto with *. apply in_eq_part. intros x0 H'2; try assumption. apply in_part_inter_l with B; auto with *. intros x0 H'2; try assumption. apply in_part_inter; auto with *. apply in_part_trans_eq with x; auto with *. Qed.
imports: Fpart Inter Arith