Lemma negimpl_to_conj (P Q:hProp) : LEM -> ( ¬ (P ⇒ Q) -> P ∧ ¬ Q ). Proof. intros lem ni. assert (r := negforall_to_existsneg _ lem ni); clear lem ni. apply (squash_to_hProp r); clear r; intros [p nq]. exact (p,,nq). Defined.