proposition: Lemma is_strincr_impl_incr {m : nat} (f : ⟦m⟧ → nat) : is_stn_strictly_increasing f -> is_stn_increasing f.
proof: Proof. intros inc ? ? e. induction (natlehchoice _ _ e) as [I|J]; clear e. + apply natlthtoleh. apply inc. exact I. + assert (J' : i = j). { apply subtypePath_prop. exact J. } clear J. induction J'. apply isreflnatleh. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions