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+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:, E:({...i}Prop). E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))	[int_lower_ind]
Thm* i:, E:({i...}Prop). E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k))	[int_upper_ind]
Thm* a:, b:. |a| = |b| (a rem b) = 0	[rem_eq_args_z]
Thm* a:, b:. |a| < |b| (a rem b) = a	[rem_base_case_z]
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:, p,q:. Div(a;n;p) Div(a;n;q) p = q	[div_unique]
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:. ij -i-j	[minus_functionality_wrt_le]
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]

In prior sections: core well fnd int 1 bool 1

Try larger context: StandardLIB