(16steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: div floor mod unique

a:, n:, q:, r:. a = qn+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:

11. a:
2. n:
3. q:
4. r:
5. a = qn+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:
intaddmultiplyless_thanequalimpliesandall

(16steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc