proposition: Lemma lef_at (aT : Type) d (T : porderType d) (f : (aT -> T)^nat) x : nondecreasing_seq f -> {homo (f^~ x) : n m / (n <= m)%N >-> (n <= m)%O}.
proof: Proof. by move=> nf m n mn; have /asboolP := nf _ _ mn; exact. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau