proposition: Lemma DN_or P Q: (((P -> False) /\ (Q -> False)) -> False) -> DN (P + Q).
proof: Proof. firstorder. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.Classes.Morphisms CoRN.reals.fast.CRGroupOps CoRN.logic.Classic