(4steps 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 com 1 1 1
1. p : 
2. q : 
  p +q q.numq +q p.den = q +q p.nump +q q.den
By: OnHyps [2;1] RatHD THEN Unfold `qadd` 0 THEN RW (DepthC qnd_evalC) 0

Generated subgoals:

None

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

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