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