proposition: Lemma Book_1_13_aux: forall A B, ~(A + B) -> ~A * ~B.
proof: Proof. intros A B nAorB; split. - intro a; exact (nAorB (inl a)). - intro b; exact (nAorB (inr b)). Qed.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)