proposition: Lemma diff_add_part2 : forall (E : Setoid) (A : part_set E) (x : E), in_part x A -> Equal A (add_part (diff A (single x)) x).
proof: Proof. intros E0 A x H'; try assumption. apply in_eq_part. intros x0 H'0; try assumption. elim (classic (Equal x x0)); intros. apply in_part_trans_eq with x; auto with *. cut (in_part x0 (diff A (single x))). unfold add_part in |- *; auto with *. apply in_diff; auto with *. intros x0 H'0; try assumption. elim (classic (Equal x x0)); intros. apply in_part_trans_eq with x; auto with *. cut (in_part x0 (diff A (single x))). intros H'1; try assumption. apply diff_in_l with (single x). auto with *. unfold add_part in H'0. elim (in_part_union H'0); intros. auto with *. absurd (Equal x x0); auto with *. Qed.
imports: Fpart2