Standard library
Theorem files
Base
Int
List
Log
Maps
MultiSet
Nat
Option
Pair
Set
Sums
Proof files
Base
Int
List
Log
Maps
MultiSet
Nat
Option
Pair
Set
Sums
Theme:
Deduce Dark
Deduce Light
VS Code Dark
VS Code Light
High Contrast
fun
log
(
n
)
{
find_log
(
n
,
0
,
0
)
}
less_equal_pow_log
:
(
all
n
:
Nat
.
n
≤
pow2
(
log
(
n
)
)
)