Nuprl - Proof: qadd functionality 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: qadd functionality 1

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

Generated subgoal:

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
5 steps

About:

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