Theorem: ZerosOnesAndTwos.digits_len' (Compfiles/ZeroesOnesAndTwos.lean)

State before:
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 n).length = 1 + (Nat.digits 10 (n / 10)).length
Tactic:
rw [Nat.digits_def' two_le_ten hn, List.length]
State after:
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 (n / 10)).length + 1 = 1 + (Nat.digits 10 (n / 10)).length

State before:
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 (n / 10)).length + 1 = 1 + (Nat.digits 10 (n / 10)).length
Tactic:
exact add_comm _ _
State after:
no goals