proposition: Lemma weqfromcoprodofstn_invmap_r0 (n : nat) (i : ⟦n+0⟧ ) : weqfromcoprodofstn_invmap n 0 i = ii1 (transportf stn (natplusr0 n) i).
proof: Proof. intros. unfold weqfromcoprodofstn_invmap. simpl. induction (natlthorgeh i n) as [I|J]. - simpl. apply maponpaths. apply subtypePath_prop. simpl. induction (natplusr0 n). apply idpath. - simpl. apply fromempty. induction (! natplusr0 n). exact (natgehtonegnatlth _ _ J (stnlt i)). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions