proposition: Lemma Seminus_Empty_set_r: forall A s, Setminus A s (Empty_set A) = s.
proof: Proof. intros. apply Extensionality_Ensembles. split. * intros x H1. destruct H1. unfold In in *. assumption. * intuition. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset