proposition: Theorem weqfromcoprodofstn (n m : nat) : (⟦n⟧ ⨿ ⟦m⟧) ≃ ⟦n+m⟧.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions