Def  == {i:| 0i }

is mentioned by

Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime]
Thm* n:. fib(n)	[fib_wf]
Thm* b:, a:. u,v:. GCD(a;b;ua+vb)	[bezout_ident_n]
Thm* b:, a:. y:. GCD(a;b;y)	[gcd_ex_n]
Thm* b:, a:. y:. GCD(a;b;y)	[gcd_exists_n]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n]
Thm* a:, b:. a | b & b | a  a<b & a | b	[pdivisor_bound]
Thm* a,b:. (a ~ b)  a = b	[assoced_nelim]
Thm* a:, b:. a | b  ab	[divisor_bound]
Thm* a,b:. a | b  b | a  a = b	[divides_anti_sym_n]
Thm* a:, b:. a | b  ab	[divisors_bound]

In prior sections: int 1 bool 1 int 2

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html