Theorem: Nat.toDigits_ne_nil (One.lean)

State before:
b n : ℕ
⊢ toDigits b n ≠ []
Tactic:
unfold Nat.toDigits
State after:
b n : ℕ
⊢ toDigitsCore b (n + 1) n [] ≠ []

State before:
b n : ℕ
⊢ toDigitsCore b (n + 1) n [] ≠ []
Tactic:
simp [Nat.toDigitsCore_ne_nil]
State after:
no goals