Lemma weqfromcoprodofstn_invmap_r0 (n : nat) (i : ⟦n+0⟧ ) : weqfromcoprodofstn_invmap n 0 i = ii1 (transportf stn (natplusr0 n) i). 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.