proposition: Lemma compl_not_compl : forall (A : part_set E) (x : E), in_part x A \/ in_part x (compl A).
proof: Proof. intros A x; try assumption. simpl in |- *. unfold not in |- *. apply NNPP; intuition. Qed.
imports: Classical_Prop Parts