| Who Cites div floor? |
|
div_floor | Def a ![](FONT/div.png) n
Def == if 0![](FONT/le.png) a a n ; ((-a) rem n)= 0 -((-a) n) else -((-a) n)+-1 fi |
| | Thm* a: , n:![](FONT/nat.png) . (a ![](FONT/div.png) n) ![](FONT/int.png) |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j) ![](FONT/bool.png) |
|
le_int | Def i![](FONT/le.png) j == ![](FONT/not.png) j< i |
| | Thm* i,j: . (i![](FONT/le.png) j) ![](FONT/bool.png) |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j) ![](FONT/bool.png) |
|
bnot | Def ![](FONT/not.png) b == if b false else true fi |
| | Thm* b: . ![](FONT/not.png) b ![](FONT/bool.png) |