k,m:
. (
f:(k
m). increasing(f;k)) 
k
mk:, f:(k
). increasing(f;k) (x,y:k. x<y f(x)<f(y))| Theorem | Name |
| k,m:. (f:(km). increasing(f;k)) km | [increasing_le] |
| cites the following: | |
| k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y)) | [increasing_implies] |