is mentioned by

Thm* k:, L: List. 0 < ||L|| (r:. r- > L^k)	[Ramsey]
Thm* k:, L: List, r1,r2:. r1r2 r1- > L^k r2- > L^k	[arrows-monotone1]
Thm* k:, L: List. k-1- > L^k (i:||L||. L[i] < k)	[trivial-arrows]
Thm* n,m:, f:((n-1)(m-1)). Inj((n-1); (m-1); f) Inj(n; m; f[n-1:=m-1])	[fappend-inject]
Thm* n,m:, f:((n-1)(m-1)). increasing(f;n-1) increasing(f[n-1:=m-1];n)	[fappend-increasing]
Thm* x:, n:. (n | x) (x mod n) = 0	[elim_divides]
Thm* x,y:, n:. ((xy) mod n) = mod_guard((x mod n)(y mod n);n)	[mod_mul_guard]
Thm* x,y:, n:. ((x+y) mod n) = mod_guard((x mod n)+(y mod n);n)	[mod_add_guard]
Def DivGraph_2 == Graph(i: -- > in | n:)	[divides-graph2]
Def DivGraph_1 == Graph(i,j:. i | j)	[divides-graph1]

In prior sections: int 1 int 2 num thy 1 mb nat graph 1 1

Try larger context: Graphs