theorem :: NUMBER14:24

for f being real-valued decreasing FinSequence holds min_p f = len f