for seq being nonnegative ExtREAL_sequence holds
( not seq is non-decreasing or seq is convergent_to_+infty or seq is convergent_to_finite_number )