proposition: Lemma add_soustr_xy : forall (X:Ensemble U) (x y:U), x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
proof: Proof. intros X x y H'; apply Extensionality_Ensembles. split; red. - intros x0 H'0; elim H'0; auto with sets. intro H'1; elim H'1. + intros u H'2 H'3; try assumption. apply Add_intro1. apply Subtract_intro; auto with sets. + intros t H'2 H'3; try assumption. elim (Singleton_inv U x t); auto with sets. - intros u H'2; try assumption. elim (Add_inv U (Subtract U X y) x u); auto with sets. + intro H'0; elim H'0; auto with sets. + intro H'0; rewrite <- H'0; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets