int 2 Sections StandardLIB Doc

Def == {i:| 0 < i }

is mentioned by

Thm* a:, n:. a = (a n)n+(a mod n)[div_floor_mod_sum]
Thm* a:, n:. 0(a mod n) & (a mod n) < n[mod_bounds]
Thm* a:, n:. (a mod n) [modulus_wf]
Thm* a:. (a rem a) = 0[rem_eq_args]
Thm* a:, n:. ((a rem n) rem n) = (a rem n)[rem_rem_to_rem]
Thm* i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)[rem_addition]
Thm* a,b:, n:. ((a+bn) rem n) = (a rem n)[rem_invariant]
Thm* a:, n:. an (a rem n) = ((a-n) rem n)[rem_rec_case]
Thm* a:, n:. a < n (a rem n) = a[rem_base_case]
Thm* a:, n:. an (a n) = ((a-n) n)+1[div_rec_case]
Thm* a:, n:. a < n (a n) = 0[div_base_case]
Thm* a:, n:. Rem(a;n;a rem n)[rem_fun_sat_rem_nrel]
Thm* a:, n:, k:. k(a n) kna[div_lbound_1]
Thm* a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = q[div_unique]
Thm* a:, n:. q:. Div(a;n;q) & (a n) = q[div_elim]
Thm* a:, n:. Div(a;n;a n)[div_fun_sat_div_nrel]
Thm* a:, n:. (a n) [divide_wf]
Thm* a:, n:. 0(a n)[div_bounds_1]
Thm* a:, n:. (a rem n) [remainder_wf]
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)[rem_2_to_1]
Thm* a:{...0}, b:. (a b) = -((-a) b)[div_2_to_1]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n[rem_bounds_2]
Thm* a:, n:. 0(a rem n) & (a rem n) < n[rem_bounds_1]
Thm* a,b:. 0 < ab[mul_bounds_1b]
Thm* a,b:, n:. nanb ab[mul_cancel_in_le]
Thm* a,b:, n:. na < nb a < b[mul_cancel_in_lt]
Thm* a,b:, n:. a < b na < nb[mul_preserves_lt]

In prior sections: int 1

Try larger context: StandardLIB

int 2 Sections StandardLIB Doc