theorem :: INTEGR26:24

for p, q being R_eal
for f being PartFunc of REAL,REAL st f is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f,x) <= 0 ) holds
f | ].p,q.[ is non-increasing