theorem Collatz.converges_3 : CollatzConverges 3

theorem Collatz.converges_5 : CollatzConverges 5

theorem Collatz.converges_6 : CollatzConverges 6

theorem Collatz.converges_7 : CollatzConverges 7

theorem Collatz.converges_8 : CollatzConverges 8

theorem Collatz.converges_9 : CollatzConverges 9

theorem Collatz.converges_10 : CollatzConverges 10

theorem Collatz.converges_11 : CollatzConverges 11

theorem Collatz.converges_12 : CollatzConverges 12

theorem Collatz.converges_13 : CollatzConverges 13

theorem Collatz.converges_14 : CollatzConverges 14

theorem Collatz.converges_15 : CollatzConverges 15

theorem Collatz.converges_16 : CollatzConverges 16

theorem Collatz.converges_17 : CollatzConverges 17

theorem Collatz.converges_18 : CollatzConverges 18

theorem Collatz.converges_19 : CollatzConverges 19

theorem Collatz.converges_20 : CollatzConverges 20

theorem Collatz.converges_le_twenty (n : ℕ) (h1 : 1 ≤ n) (h2 : n ≤ 20) : CollatzConverges n