Theorem: ZerosOnesAndTwos.prepend_two_pos (Compfiles/ZeroesOnesAndTwos.lean)

State before:
n : ℕ
⊢ 0 < prepend_two n
Tactic:
cases n
State after:
case zero

⊢ 0 < prepend_two 0

case succ
n✝ : ℕ
⊢ 0 < prepend_two (n✝ + 1)

State before:
case zero

⊢ 0 < prepend_two 0
Tactic:
norm_num [prepend_two]
State after:
no goals

State before:
case succ
n✝ : ℕ
⊢ 0 < prepend_two (n✝ + 1)
Tactic:
rw [prepend_two]
State after:
case succ
n✝ : ℕ
⊢ 0 < 2 * 10 ^ (Nat.digits 10 (n✝ + 1)).length + (n✝ + 1)

State before:
case succ
n✝ : ℕ
⊢ 0 < 2 * 10 ^ (Nat.digits 10 (n✝ + 1)).length + (n✝ + 1)
Tactic:
norm_num
State after:
no goals