proposition: Lemma fromneganddecx {X Y : UU} : isdecprop X -> ¬ (X × Y) -> ¬X ⨿ ¬Y.
proof: 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.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom