(4steps 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: mul cancel in assoced

  a,b:n:. ((na) ~ (nb))  (a ~ b)

By: UnivCD
THEN
(OnMCls [0;-1] (RWH (LemmaC Thm* a,b:. (a ~ b a = b  a = -b)))


Generated subgoal:

1 1. a : 
2. b : 
3. n : 
4. na = nb  na = -nb
  a = b  a = -b

3 steps

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

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