(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub mul 1
1. b : 
2. c : 
3. 0b = c
  (0b) ~ c
By: Rewrite by c = 0  

Generated subgoal:

1   (0b) ~ 0
2 steps

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

(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc