theorem Collatz.collatz_pow_two_succ (k : ℕ) : collatz (2 ^ (k + 1)) = 2 ^ k

theorem Collatz.converges_pow_two (k : ℕ) : CollatzConverges (2 ^ k)

theorem Collatz.trajectory_pow_two (k : ℕ) : collatz^[k] (2 ^ k) = 1