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