Rank | Theorem | Name |
4 |
Thm* ![]() ![]() ![]() ![]() ![]() | [div_2_to_1] |
cites | ||
0 |
Thm* ![]() ![]() ![]() ![]() | [rem_bounds_2] |
0 |
Thm* ![]() ![]() ![]() ![]() ![]() | [rem_bounds_1] |
0 |
Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [div_rem_sum] |
1 |
Thm* ![]() ![]() ![]() ![]() | [add_mono_wrt_eq] |
3 |
Thm* ![]() ![]() ![]() ![]() | [add_mono_wrt_lt] |
2 |
Thm* ![]() ![]() ![]() ![]() ![]() ![]() | [add_mono_wrt_le] |
0 | Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [lt_transitivity_1] |
2 |
Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [mul_cancel_in_lt] |