(2steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
rem
self
n:
. (n rem n) = 0
By:
Auto
THEN
Inst
Thm*
a:
, n:
, q,r:
. a = q
n+r
|r| < |n|
(r < 0
a < 0)
(r > 0
a > 0)
q = (a
n) & r = (a rem n) [n;n;1;0]
Generated subgoal:
1
1.
n:
|0| < |n|
1
step
About:
(2steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
|0| < |n|
n:
n+r 
|r| < |n| 
n) & r = (a rem n)
[n;n;1;0]
