1. p : 
2. q : 
3. r : 
4. s : 
  p =q q  r =q s  p *q r =q q *q s

By:	Unfold `eq_rat` 0 THEN RWH (LemmaC Thm* x,y:. x=y  x = y) 0

1

p.numq.den = q.nump.den      r.nums.den = s.numr.den  p *q r.numq *q s.den = q *q s.nump *q r.den

4 steps

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