is mentioned by

Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k))	[decidable__all_int_seg]
Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k))	[decidable__ex_int_seg]
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x > y)	[int_seg_well_founded_down]
Thm* i:, j:{i+1...}, E:({i..j}Prop). E(i) (k:{(i+1)..j}. E(k-1) E(k)) (k:{i..j}. E(k))	[int_seg_ind]
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x < y)	[int_seg_well_founded_up]
Thm* i:, E:({...i}Prop). E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))	[int_lower_ind]
Thm* n:. WellFnd{i}({...n};x,y.x > y)	[int_lower_well_founded]
Thm* i:, E:({i...}Prop). E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k))	[int_upper_ind]
Thm* n:. WellFnd{i}({n...};x,y.x < y)	[int_upper_well_founded]
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:, b:. |a| = |b| (a rem b) = 0	[rem_eq_args_z]
Thm* a:. (a rem a) = 0	[rem_eq_args]
Thm* a:, b:. |a| < |b| (a rem b) = a	[rem_base_case_z]
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_gen_base_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_wfa]
Thm* a:, n:. (a n)	[divide_wf]
Thm* a:, n:. 0(a n)	[div_bounds_1]
Thm* a:, n:. |a rem n| < |n|	[rem_mag_bound]
Thm* a:, n:. (a rem n) = (a rem -n)	[rem_sym_2]
Thm* a:, n:. (a rem n) = -((-a) rem n)	[rem_sym_1a]
Thm* a:, n:. -(a rem n) = ((-a) rem n)	[rem_sym_1]
Thm* a:, b:. |a rem b| < |b|	[rem_bounds_z]
Thm* a:, n:. (a rem n)	[remainder_wf]
Thm* a:, b:. ((-a) rem b) = -(a rem b)	[rem_antisym]
Thm* a:, b:. (a rem -b) = (a rem b)	[rem_sym]
Thm* a:, n:{...-1}. (a rem n) = (a rem -n)	[rem_4_to_1]
Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)	[rem_3_to_1]
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)	[rem_2_to_1]
Thm* a:, b:{...-1}. (a b) = -(a (-b))	[div_4_to_1]
Thm* a:{...0}, b:{...-1}. (a b) = ((-a) (-b))	[div_3_to_1]
Thm* a:{...0}, b:. (a b) = -((-a) b)	[div_2_to_1]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n) < -n	[rem_bounds_4]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n	[rem_bounds_3]
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:, n:. (a rem n) = a-(a n)n	[rem_to_div]
Thm* a:, n:. a = (a n)n+(a rem n)	[div_rem_sum]
Thm* a,b:. (a -- b) = 0 ab	[ndiff_zero]
Thm* a,b:. (a -- b)+b = imax(a;b)	[ndiff_add_eq_imax]
Thm* a,b:. (a -- (a -- b)) = imin(a;b)	[ndiff_ndiff_eq_imin]
Thm* a,b:, c:. ((a -- b) -- c) = (a -- (b+c))	[ndiff_ndiff]
Thm* a:, b:. ((a+b) -- b) = a	[ndiff_inv]
Thm* a:. (0 -- a) = 0	[ndiff_ann_l]
Thm* a:. (a -- 0) = a	[ndiff_id_r]
Thm* a,b,c:. aimin(b;c) ab & ac	[imin_ub]
Thm* a,b,c:. imin(a;b)c ac bc	[imin_lb]
Thm* a,b,c:. imin(a;b)+c = imin(a+c;b+c)	[imin_add_r]
Thm* a,b:. imin(a;b) = imin(b;a)	[imin_com]
Thm* a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c)	[imin_assoc]
Thm* a,b:. imax(a;b) = imax(b;a)	[imax_com]
Thm* a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)	[imax_assoc]
Thm* a,b,c:. imax(a;b)+c = imax(a+c;b+c)	[imax_add_r]
Thm* a,b,c:. aimax(b;c) ab ac	[imax_ub]
Thm* a,b,c:. imax(a;b)c ac & bc	[imax_lb]
Thm* a,b:. -imin(a;b) = imax(-a;-b)	[minus_imin]
Thm* a,b:. -imax(a;b) = imin(-a;-b)	[minus_imax]
Thm* P:(Prop). (x:. P(|x|)) (x:. P(x))	[absval_elim]
Thm* i:. |i| = |-i|	[absval_sym]
Thm* x,y:. |x| = |y| x = y	[absval_eq]
Thm* i:, n:. |i| > n i < -n i > n	[absval_lbound]
Thm* i:, n:. |i|n -ni & in	[absval_ubound]
Thm* i:. |i| = 0 i = 0	[absval_zero]
Thm* i:{...0}. |i| = -i	[absval_neg]
Thm* i:. |i| = i	[absval_pos]
Thm* x:. |x|	[absval_wf]
Thm* i,j:. ij	[multiply_nat_wf]
Thm* a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0	[neg_mul_arg_bounds]
Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0	[pos_mul_arg_bounds]
Thm* a,b:. 0 < ab	[mul_bounds_1b]
Thm* a,b:. 0ab	[mul_bounds_1a]
Thm* a,b:. a 0 b 0 ab 0	[int_entire_a]
Thm* a,b:. ab = 0 a = 0 b = 0	[int_entire]
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2	[multiply_functionality_wrt_le]
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:. na = nb a = b	[mul_cancel_in_eq]
Thm* a,b:, n:. ab nanb	[mul_preserves_le]
Thm* a,b:, n:. a < b na < nb	[mul_preserves_lt]
Thm* a,b:. ab = 0 a = 0 & b = 0	[zero_ann_b]
Thm* a,b:. a = 0 b = 0 ab = 0	[zero_ann_a]
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1-i2j1-j2	[sub_functionality_wrt_le]
Thm* i,j:. i > j -i < -j	[minus_mono_wrt_lt]
Thm* i,j:. ij -i-j	[minus_functionality_wrt_le]
Thm* a,b,n:. ab a+nb+n	[add_mono_wrt_le_rw]
Thm* a,b,n:. ab a+nb+n	[add_mono_wrt_le]
Thm* a,b,n:. a < b a+n < b+n	[add_mono_wrt_lt_rw]
Thm* a,b,n:. a < b a+n < b+n	[add_mono_wrt_lt]
Thm* a,b,n:. a = b a+n = b+n	[add_mono_wrt_eq_rw]
Thm* a,b,n:. a = b a+n = b+n	[add_mono_wrt_eq]
Thm* a,b,n:. a+nb+n ab	[add_cancel_in_le]
Thm* a,b,n:. a+n < b+n a < b	[add_cancel_in_lt]
Thm* a,b,n:. a+n = b+n a = b	[add_cancel_in_eq]
Thm* i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2	[add_functionality_wrt_lt]
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2	[add_functionality_wrt_le]
Thm* i,j:. ij i < j+1	[le_to_lt_rw]
Thm* i,j:. i < j i+1j	[lt_to_le_rw]

In prior sections: core well fnd int 1 bool 1

Try larger context: StandardLIB