proposition: Lemma stnlt {n : nat} (i:stn n) : i < n.
proof: Proof. intros. exact (pr2 i). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions