Nuprl - Proof: compose increasing 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose increasing 1

1. k :

2. m :

3. f :

m
4. g :

5. increasing(f;k)
6. increasing(g;m)
7. i :

(k-1)

g(f(i))<g(f(i+1))

By:	FwdThru Thm* k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y)) [-2] THEN BackThru -1

Generated subgoal:

1 8. x,y:m. x<y g(x)<g(y)
f(i)<f(i+1)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html