proposition: Fact Add_Subtract_discouraging {X : Type} U (x : X) : Same_set U (Add (Subtract U x) x) <-> In U x /\ forall y : X, In U y -> x = y \/ x <> y.
proof: Proof. split. - intros HU. split. { rewrite HU; right; constructor. } intros y Hy. rewrite HU in Hy. destruct Hy as [y Hy|y Hy]; [right|left]. + destruct Hy as [_ Hy]. intros ?. subst. apply Hy. constructor. + destruct Hy. reflexivity. - intros [Hx HU]. split; red. + intros y Hy. specialize (HU y Hy) as [|]. * subst. right. constructor. * left. split; [assumption|]. intros Hq; destruct Hq; contradiction. + intros y Hy. destruct Hy as [y Hy|y Hy]; destruct Hy; assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) Coq(Morphisms Setoid)