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* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n	[div_floor_mod_properties]
Thm* a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)	[div_rem_properties]
Thm* n:, P:((n+1)Prop). (x:(n+1). P(x)) P(0) & (x:n. P(x+1))	[all-nsub-add1]
Thm* L:(A+B) List, a:A. mapoutl(L) = [a] (L1,L2:(A+B) List. L = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)	[mapoutl_is_singleton]
Thm* L:(A+B) List, l1,l2:A List. mapoutl(L) = (l1 @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2)	[mapoutl_is_append]
Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y))	[member_mapoutl]
Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) ||A|| < ||B||	[length_less]
Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)	[no_repeats_append_iff]
Thm* a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b)	[l_disjoint_append2]
Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c)	[l_disjoint_append]
Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a)	[l_disjoint_cons2]
Thm* a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b)	[l_disjoint_cons]
Thm* x,z,y,w:T List. ||x|| = ||z|| ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w	[append_one_one]
Thm* a,b:T List, x:T. [x] = (a @ b) a = nil & b = [x] b = nil & a = [x]	[append_is_singleton]
Thm* a,c,b,d:T List. (a @ b) = (c @ d) (e:T List. a = (c @ e) & d = (e @ b) c = (a @ e) & b = (e @ d))	[equal_appends]
Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B))	[l_before_decomp]
Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)	[l_before_append_iff]
Thm* C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B)	[sublist_append_iff]
Thm* (x,y:T. Dec(x = y)) (s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]) & (z s1)))	[l_member_decomp2]
Thm* l1,l2:T List. nil = (l1 @ l2) l1 = nil & l2 = nil	[nil_is_append]
Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))	[inverse-biject]
Thm* i,j,k:. (k upto(i;j)) ik & k < j	[member_upto]
Thm* x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3	[equal_appends_eq]
Thm* x1,z,x2,x3:T List. ||z||||x1|| (x1 @ x2) = (z @ x3) (z':T List. x1 = (z @ z') & x3 = (z' @ x2))	[equal_appends_case2]
Thm* x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3))	[equal_appends_case1]

In prior sections: core int 1 bool 1 int 2 mb nat mb list 1 num thy 1 mb list 2 fun 1 rel 1

Try larger context: Graphs