case pos
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : m = 0
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q

case neg
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : ¬m = 0
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
by_cases hm : m = 0
case neg
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : ¬m = 0
⊢ List.getLast (m % b :: digits b (m / b)) (_ : m % b :: digits b (m / b) ≠ []) = List.getLast (digits b (m / b)) q
case neg
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : ¬m = 0
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
simp only [digits_eq_cons_digits_div h hm]
no goals
case neg
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : ¬m = 0
⊢ List.getLast (m % b :: digits b (m / b)) (_ : m % b :: digits b (m / b) ≠ []) = List.getLast (digits b (m / b)) q
rw [List.getLast_cons]
no goals
case pos
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : m = 0
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
simp [hm]