proposition: Lemma increasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) : (forall n, u_ n < u_ n.+1)%O <-> increasing_seq u_.
proof: Proof. split; first by move=> u_nondec; apply: le_mono; apply: homo_ltn lt_trans _. by move=> u_incr n; rewrite lt_neqAle eq_le !u_incr leqnSn ltnn. 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