proposition: Lemma disjoint_diff : forall A B : part_set E, disjoint A (diff B A).
proof: Proof. red in |- *. intros A B; try assumption. apply not_in_empty. intros x; red in |- *; intros H'; try exact H'. absurd (in_part x A). apply diff_in_r with B. auto with *. apply in_part_inter_r with A; auto with *. apply in_part_inter_l with (diff B A); auto with *. Qed.
imports: Fpart Inter Arith