Lemma dneg_elim_to_LEM : (∏ P:hProp, ¬ ¬ P -> P) -> LEM. 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.