Documentation
Collatz
.
Descent
Search
return to top
source
Imports
Init
Collatz.Basic
Imported by
Collatz
.
collatz_even_lt
Collatz
.
collatz_odd_gt
source
theorem
Collatz
.
collatz_even_lt
{
n
:
ℕ
}
(
hn
:
0
<
n
)
(
he
:
n
%
2
=
0
)
:
collatz
n
<
n
source
theorem
Collatz
.
collatz_odd_gt
{
n
:
ℕ
}
(
hn
:
0
<
n
)
(
ho
:
n
%
2
=
1
)
:
collatz
n
>
n