Definition weqfromcoprodofstn_invmap (n m : nat) : ⟦n + m⟧ -> (⟦n⟧ ⨿ ⟦m⟧). Proof. intros i. induction (natlthorgeh i n) as [i1 | i2]. - exact (ii1 (make_stn n i i1)). - exact (ii2 (make_stn m (i - n) (nat_split (pr2 i) i2))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.