int 2 Sections StandardLIB Doc

RankTheoremName
4 Thm* a:{...0}, b:. (a b) = -((-a) b)[div_2_to_1]
cites
0 Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n[rem_bounds_2]
0 Thm* a:, n:. 0(a rem n) & (a rem n) < n[rem_bounds_1]
0 Thm* a:, n:. a = (a n)n+(a rem n)[div_rem_sum]
1 Thm* a,b,n:. a = b a+n = b+n[add_mono_wrt_eq]
3 Thm* a,b,n:. a < b a+n < b+n[add_mono_wrt_lt]
2 Thm* a,b,n:. ab a+nb+n[add_mono_wrt_le]
0Thm* i,j,k:. i < j jk i < k[lt_transitivity_1]
2 Thm* a,b:, n:. na < nb a < b[mul_cancel_in_lt]

int 2 Sections StandardLIB Doc