is mentioned by

Thm* k1,k2:. f:((k1+k2)(k1+k2)). Inj(k1+k2; (k1+k2); f)	[union_cardinality1]
Thm* n:, f:(n). increasing(f;n) (i:n, j:i. f(j) (f(i)))	[increasing-implies2]
Thm* k:, f,g:(k), p:(k). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)	[sum-ite]
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* n:, P:((n+1)Prop). (x:(n+1). P(x)) P(0) & (x:n. P(x+1))	[all-nsub-add1]
Thm* s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f))	[no_repeats_inj]
Thm* i,j:, k:(j-i). upto(i;j)[k] = i+k	[select_upto]
Thm* j:, i:j. ||upto(i;j)|| = j-i	[length_upto]
Thm* i,j:. upto(i;j) {i..j} List	[upto_wf]
Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))	[assert_l_bexists]
Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))	[assert_l_ball]

In prior sections: int 1 bool 1 int 2 list 1 mb basic mb nat mb list 1 num thy 1 mb list 2 prog 1

Try larger context: Graphs