Lemma tonegdirprod {X Y : UU} : ¬ X ∨ ¬ Y -> ¬ (X × Y). Proof. simpl. apply (@hinhuniv _ (make_hProp _ (isapropneg (X × Y)))). intro c. induction c as [ nx | ny ]. - simpl. intro xy. apply (nx (pr1 xy)). - simpl. intro xy. apply (ny (pr2 xy)). Defined.