proposition: Lemma nonincreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) : (forall n, u_ n >= u_ n.+1)%O <-> nonincreasing_seq u_.
proof: Proof. split; first by apply: homo_leq (fun _ _ _ u v => le_trans v u). by move=> u_nincr n; exact: u_nincr. 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