:: deftheorem defines non-descending PROB_1:def 5 :
for f being Function holds
( f is non-descending iff for n, m being Nat st n <= m holds
f . n c= f . m );