Lemma stn_ord_incl {m : nat} (f : ⟦S m⟧ → nat) : is_stn_strictly_increasing f → f lastelement ≥ f firstelement + m. Proof. intros strinc. assert (inc := is_strincr_impl_incr _ strinc). set (d := λ i : ⟦ m ⟧, f (dni_firstelement i) - f (dni_lastelement i)). assert (E := stnsum_diffs f inc). change (stnsum d = f lastelement - f firstelement) in E. assert (F : ∏ i, f (dni_firstelement i) > f (dni_lastelement i)). { intros i. apply strinc. change (stntonat _ i < S(stntonat _ i)). apply natlthnsn. } assert (G : ∏ i, d i ≥ 1). { intros i. apply natgthtogehsn. apply minusgth0. apply F. } clear F. assert (H := stnsum_ge1 _ G). clear G. rewrite E in H. clear E d. assert (I : f lastelement ≥ f firstelement). { apply inc. apply idpath. } assert (J := minusplusnmm _ _ I); clear I. rewrite <- J; clear J. rewrite natpluscomm. apply natgehandplusl. exact H. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.