is mentioned by

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* 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* i:{...0}. |i| = -i	[absval_neg]

In prior sections: int 1

Try larger context: StandardLIB