Lemma weak_fromnegdirprod (P Q: hProp) : ¬ (P ∧ Q) -> ¬¬(¬ P ∨ ¬ Q). Proof. intros npq k. assert (e : ¬¬ Q). { intro n. apply k. apply hdisj_in2. assumption. } assert (d : ¬¬ P). { intro n. apply k. apply hdisj_in1. assumption. } clear k. apply d; clear d. intro p. apply e; clear e. intro q. refine (npq _). exact (p,,q). Defined.