proposition: Lemma negimpl_to_conj (P Q:hProp) : LEM -> ( ¬ (P ⇒ Q) -> P ∧ ¬ Q ).
proof: 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.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions