n b m : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2) → ∀ {d : ℕ}, d ∈ digits (b + 2) n → d < b + 2
n b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
apply Nat.strongInductionOn m
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
d : ℕ
hd : d ∈ digits (b + 2) n
⊢ d < b + 2
n b m : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2) → ∀ {d : ℕ}, d ∈ digits (b + 2) n → d < b + 2
intro n IH d hd
case zero
n b m d : ℕ
IH : ∀ (m : ℕ), m < zero → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ digits (b + 2) zero
⊢ d < b + 2

case succ
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ digits (b + 2) (succ n)
⊢ d < b + 2
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
d : ℕ
hd : d ∈ digits (b + 2) n
⊢ d < b + 2
cases' n with n
case succ
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: digits (b + 2) ((n + 1) / (b + 2))
⊢ d < b + 2
case succ
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ digits (b + 2) (succ n)
⊢ d < b + 2
rw [digits_add_two_add_one] at hd
case succ.head
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
⊢ (n + 1) % (b + 2) < b + 2

case succ.tail
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d < b + 2
case succ
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: digits (b + 2) ((n + 1) / (b + 2))
⊢ d < b + 2
cases hd
case zero
n b m d : ℕ
IH : ∀ (m : ℕ), m < zero → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ []
⊢ d < b + 2
case zero
n b m d : ℕ
IH : ∀ (m : ℕ), m < zero → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ digits (b + 2) zero
⊢ d < b + 2
rw [digits_zero] at hd
no goals
case zero
n b m d : ℕ
IH : ∀ (m : ℕ), m < zero → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ []
⊢ d < b + 2
cases hd
no goals
case succ.head
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
⊢ (n + 1) % (b + 2) < b + 2
exact n.succ.mod_lt (by simp)
no goals
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
⊢ b + 2 > 0
simp
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < succ n

case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d ∈ digits (b + 2) ((n + 1) / (b + 2))
case succ.tail
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d < b + 2
apply IH ((n + 1) / (b + 2))
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d ∈ digits (b + 2) ((n + 1) / (b + 2))
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < succ n

case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d ∈ digits (b + 2) ((n + 1) / (b + 2))
. apply Nat.div_lt_self <;> simp
no goals
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d ∈ digits (b + 2) ((n + 1) / (b + 2))
. assumption
no goals
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < succ n
apply Nat.div_lt_self <;> simp
no goals
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d ∈ digits (b + 2) ((n + 1) / (b + 2))
assumption