Nuprl - Proof: div inverts nat mul 1 1

(5steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: div inverts nat mul 1 1

1. x :

2. y :

3. z :

4. x = y

z
5. x = (x

z)

z+(x rem z)
6. (x rem z)

z

(x

z) = y

By:	Inst: Thm* k:, q1,q2:, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 Using:[z \| y \| x z \| 0 \| x rem z] ...w

Generated subgoals:

1   yz+0 = (x  z)z+(x rem z)
Auto

2 7. y = (x  z) & 0 = (x rem z)
  (x  z) = y
Auto

About:

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

(5steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc