(12steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime elim 1 1 1 2 2

1. p : 
2. prime(p)
3. p = 0
4. (p ~ 1)
5. b,c:. (b ~ 1)  (c ~ 1)  p = bc
6. a : 
7. c : 
8. p = ac
9. a = 0
10. c = 0
  (a ~ 1)  (a ~ p)


By: (InstHyp [a;c] 5) THEN ProveProp1


Generated subgoal:

1 11. c ~ 1
  (a ~ 1)  (a ~ p)

4 steps

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

(12steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc