1. a : 
2. 0<a
3. b,c:. (a-1)b = c  (((a-1)b) ~ c)
4. b : 
5. c : 
6. ab = c
  (((a-1)b)+b) ~ c

By:	1bab  By BackThru: Thm*  i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2

1

7. 1bab   (((a-1)b)+b) ~ c

2 steps

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