proposition: Lemma not_in_comp_r : forall (E : Setoid) (A B : part_set E) (x : E), ~ in_part x A -> Equal A B -> ~ in_part x B.
proof: Proof. unfold not in |- *. intros E0 A B x H' H'0 H'1; try assumption. apply H'. apply in_part_comp_r with B; auto with algebra. Qed.
imports: Classical_Prop Parts