n)
n
a4. (a rem n)+(a
n)n < n+(a n)n
n(a n) a < n((a n)+1)
n)n(a rem n)+(a n)n n)n < n+(a n)n n(a n) a < n((a n)+1)
a,b:
. a+b = b+a)
THENC
HigherC
(RevLemmaC
Thm* a:, n:
. a = (a n)n+(a rem n)))
3| 1 | 3. 0+(a n)na 4. (a rem n)+(a n)n < n+(a n)n n(a n) a < n((a n)+1) |
About:
 |  |  |  |  |  |