is mentioned by

Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n)	[div_floor_mod_unique]
Thm* a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n)	[div_rem_unique]
Thm* x,z,y,w:T List. ||x|| = ||z|| ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w	[append_one_one]
Thm* x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3	[equal_appends_eq]

In prior sections: core well fnd int 1 bool 1 int 2 list 1 rel 1 mb nat mb list 1 num thy 1 mb list 2 sqequal 1

Try larger context: Graphs