proposition: Lemma nondecreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) : (forall n, u_ n <= u_ n.+1)%O <-> nondecreasing_seq u_.
proof: Proof. by split=> [|h n]; [exact: homo_leq le_trans | exact: h]. 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