Lemma fromneganddecx {X Y : UU} : isdecprop X -> ¬ (X × Y) -> ¬X ⨿ ¬Y. Proof. intros isx nf. induction (pr1 isx) as [ x | nx ]. - assert (ny := negf (λ y : Y, make_dirprod x y) nf). exact (ii2 ny). - exact (ii1 nx). Defined.