(16steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
div
floor
mod
unique
a:
, n:
, q:
, r:
. a = q
n+r
r < n
q = (a
n) & r = (a mod n)
By:
Auto
THEN
Inst
Thm*
a:
, n:
. a = (a
n)
n+(a mod n) & (a mod n) < n [a;n]
Generated subgoal:
1
1.
a:
2.
n:
3.
q:
4.
r:
5.
a = q
n+r
6.
r < n
7.
a = (a
n)
n+(a mod n)
8.
(a mod n) < n
q = (a
n) & r = (a mod n)
15
steps
About:
(16steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc