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* 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* n:, a,b:. sum(a+bi | i < n) = ((n(a+a+b(n-1))) 2)	[sum_arith]
Thm* n:, a,b:. sum(a+bi | i < n)2 = n(a+a+b(n-1))	[sum_arith1]
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* i,j:. no_repeats(;upto(i;j))	[no_repeats_upto]
Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))	[primrec_list_accum]
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* 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,k:. (k upto(i;j)) ik & k < j	[member_upto]
Thm* i,j:. upto(i;j) {i..j} List	[upto_wf]

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

Try larger context: Graphs