Definition stn_right (m n : nat) : ⟦n⟧ -> ⟦m+n⟧. Proof. intros i. exists (m+pr1 i). apply natlthandplusl. exact (pr2 i). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.