proposition: Lemma diff_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 (diff A B) (add_part (diff B0 B) x).
proof: Proof. intros A B0 B x H' H'0 H'1; try assumption. apply in_eq_part. intros x0 H'2; try assumption. elim (classic (Equal x0 x)). intros H'3; try assumption. apply in_part_trans_eq with x; auto with *. intros H'3; try assumption. unfold add_part in |- *. apply in_part_union_or. left. apply in_diff. apply add_part_in_el_diff with x; auto with *. apply in_part_comp_r with A; auto with *. apply diff_in_l with B; auto with *. apply diff_in_r with A; auto with *. intros x0 H'2; try assumption. apply in_diff. apply in_part_comp_r with (add_part B0 x); auto with *. elim (classic (Equal x0 x)). intros H'3; try assumption. apply in_part_trans_eq with x; auto with *. intros H'3; try assumption. unfold add_part in |- *. apply in_part_union_or. left. unfold add_part in H'2. elim (in_part_union H'2). intros H'4; try assumption. apply diff_in_l with B; auto with *. intros H'4; try assumption. absurd (in_part x0 (single x)); auto with *. elim (classic (Equal x0 x)). intros H'3; try assumption. unfold not in |- *; intros. unfold not in H'1. apply H'1. apply in_part_trans_eq with x0; auto with *. intros H'3; try assumption. apply diff_in_r with B0; auto with *. apply add_part_in_el_diff with x; auto with *. Qed.
imports: Fpart Inter Arith