proposition: Lemma dneg_elim_to_LEM : (∏ P:hProp, ¬ ¬ P -> P) -> LEM.
proof: Proof. intros dne. intros P. simple refine (dne (_,,_) _). simpl. intros n. assert (q : ¬ (P ∨ ¬ P)). { now apply weqnegtonegishinh. } assert (r := fromnegcoprod_prop q). exact (pr2 r (pr1 r)). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions