proposition: Lemma Sub_Add_new : forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
proof: Proof. auto using incl_soustr_add_l with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets