Lemma is_strincr_impl_incr {m : nat} (f : ⟦m⟧ → nat) : is_stn_strictly_increasing f -> is_stn_increasing f. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.