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