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 rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)	[div_rem_properties]
Thm* n:, f:(n). increasing(f;n) (i:n, j:i. f(j) (f(i)))	[increasing-implies2]
Thm* f:(AB), g:(BC). Inj(A; B; f) Inj(B; C; g) Inj(A; C; g o f)	[compose_inject]
Thm* k,b:, f:(k). (x:k. bf(x)) bksum(f(x) | x < k)	[sum_lower_bound]
Thm* k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)bk	[sum_bound]
Thm* k:, f,g:(k). (x:k. f(x)g(x)) sum(f(x) | x < k)sum(g(x) | x < k)	[sum_le]
Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))	[no_repeats_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* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||||B||	[length_le]
Thm* s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f))	[no_repeats_inj]
Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y L f(x) before f(y) mapfilter(f;P;L)	[mapfilter_before]
Thm* f:(TT'), x,y:T, s:T List. x before y s f(x) before f(y) map(f;s)	[map_before]
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* R:(AA'Prop), P:(BA), P':(BA'), F,G,H:(BAA), F',G',H':(BA'A'), N:(BA(B List)), N':(BA'(B List)), M:(A), M':(A'). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (i:B, s:A'. P'(i,s) M'(F'(i,s))M'(s)) (i:B, s:A'. M'(G'(i,s))M'(s)) (i:B, s:A'. P'(i,s) M'(H'(i,s)) < M'(s)) (j:B, u:A, v:A'. R(u,v) (P(j,u) P'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(F(j,u),F'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(H(j,u),H'(j,v))) (j:B, u:A, v:A'. R(u,v) R(G(j,u),G'(j,v))) (j:B, u:A, v:A'. R(u,v) N(j,u) = N'(j,v)) (j:B, u:A, v:A'. R(u,v) R(process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ,process v j where process s i == if P'(i,s) then F'(i,s) else G'(i,s) where xs := N'(i,s); s:= H'(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ))	[accumulate-rel]
Thm* M:(A), Q:(BAAProp), P:(BA), F,G,H:(BAA), N:(BA(B List)). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. P(j,u) Q(j,u,F(j,u))) (j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))) (j:B, u:A. Q(j,u,u)) (i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)) (j:B, u:A. Q(j,u,process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ))	[accumulate-induction1]
Thm* A,B:Type, P:(BA), F,G,H:(BAA), N:(BA(B List)), M:(A). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } {s:A| M(s)M(u) })	[accumulate_wf]
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* s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]))	[l_member_decomp]
Thm* s:T List. 0 < ||s|| (s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]]))	[list-decomp-last]
Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))	[inverse-biject]
Thm* f:(AB), g:(BC). Bij(A; B; f) Bij(B; C; g) Bij(A; C; g o f)	[compose-biject]
Thm* x,y:A+B. (a1,a2:A. Dec(a1 = a2)) (b1,b2:B. Dec(b1 = b2)) Dec(x = y)	[decidable__equal_union]
Thm* i,j,k:. ij jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))	[append_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 fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 union prog 1 rel 1 mb basic mb nat mb list 1 num thy 1 mb list 2

Try larger context: Graphs