theorem Collatz.collatz_cycle : collatz^[3] 1 = 1

theorem Collatz.one_isPeriodicPt : Function.IsPeriodicPt collatz 3 1

theorem Collatz.collatz_fixedPt_zero (n : ℕ) : collatz n = n ↔ n = 0

theorem Collatz.converges_one : CollatzConverges 1

theorem Collatz.converges_two : CollatzConverges 2

theorem Collatz.converges_four : CollatzConverges 4