PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
mod
self
n:
. (n mod n) = 0
By:
Auto
THEN
Inst
Thm*
a:
, n:
, q:
, r:
. a = q
n+r
r < n
q = (a
n) & r = (a mod n) [n;n;1;0]
Generated subgoals:
None
About:
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
n:
. (n mod n) = 0
a:
, n:, q:, r:. a = q
n+r 
r < n q = (a 
n) & r = (a mod n)
[n;n;1;0]