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

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

⊢ 0 < prepend_one 0

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

State before:
case zero

⊢ 0 < prepend_one 0
Tactic:
simp [prepend_one]
State after:
no goals

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

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