Nuprl - Proof: qadd assoc 1

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

1. p :

2. q :

3. r :

p +q q +q r =q p +q q +q r

By:	Unfold `eq_rat` 0

Generated subgoal:

1 p +q q +q r.nump +q q +q r.den=p +q q +q r.nump +q q +q r.den
3 steps

About:

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