Nuprl - Proof: compose increasing

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

k,m:

, f:(

m), g:(

increasing(f;k)

increasing(g;m)

increasing(g o f;k)

By:	Auto THEN Unfold `increasing` 0 THEN Reduce 0

Generated subgoal:

1 1. k :
2. m :
3. f : km
4. g : m
5. increasing(f;k)
6. increasing(g;m)
7. i : (k-1)
g(f(i))<g(f(i+1))
2 steps

About:

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