(7steps total) PrintForm Definitions Lemmas rat 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: qadd functionality 1 1

1. p : 
2. q : 
3. r : 
4. s : 
  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


By: OnHyps [4;3;2;1] RatHD THEN RW (SweepDnC qnd_evalC) 0


Generated subgoal:

1 1. p1 : 
2. p2 : 
3. q1 : 
4. q2 : 
5. r1 : 
6. r2 : 
7. s1 : 
8. s2 : 
  p1q2 = q1p2
  
  r1s2 = s1r2
  
  p1/p2 +q r1/r2.numq1/q2 +q s1/s2.den = q1/q2 +q s1/s2.nump1/p2 +q r1/r2.den

4 steps

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

(7steps total) PrintForm Definitions Lemmas rat 1 Sections StandardLIB Doc