Rank | Theorem | Name |
5 | Thm* a: , n:![](FONT/int.png) ![](FONT/minus.png) . |a|<|n| ![](FONT/eq.png) (a rem n) = a | [rem_gen_base_case] |
cites the following: |
3 | Thm* a: , n:![](FONT/nat.png) . a<n ![](FONT/eq.png) (a rem n) = a | [rem_base_case] |
4 | Thm* a: , b:![](FONT/int.png) ![](FONT/minus.png) . ((-a) rem b) = -(a rem b) | [rem_antisym] |
3 | Thm* a: , b:![](FONT/int.png) ![](FONT/minus.png) . (a rem -b) = (a rem b) | [rem_sym] |
0 | Thm* i: . |i| = |-i| | [absval_sym] |