fact: Definition stnmtostnn ( m n : nat ) (isnatleh: natleh m n ) : ⟦m⟧ -> ⟦n⟧ := λ x : ⟦m⟧, match x with tpair _ i is => make_stn _ i ( natlthlehtrans i m n is isnatleh ) end.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions