Theorem weqfromcoprodofstn (n m : nat) : (⟦n⟧ ⨿ ⟦m⟧) ≃ ⟦n+m⟧. Proof. use (tpair _ (weqfromcoprodofstn_map n m)). use (isweq_iso _ (weqfromcoprodofstn_invmap n m)). - exact (weqfromcoprodofstn_eq1 n m). - exact (weqfromcoprodofstn_eq2 n m). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.