case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l ∧ 1 < b ∧ 0 < m
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
rcases h with ⟨h, b2, m0⟩
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
have b0 : 0 < b := by linarith
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
have n0 : 0 < n := by linarith [mul_pos b0 m0]
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ digits b n = r :: l
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
refine' ⟨_, b2, n0⟩
case intro.intro.intro
n✝ b n : ℕ
l : List ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
h : digits b (n / b) = l
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ digits b n = n % b :: l
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ digits b n = r :: l
obtain ⟨rfl, rfl⟩ := (Nat.div_mod_unique b0).2 ⟨e, hr⟩
case intro.intro.intro
n✝ b n : ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ digits b n = n % b :: digits b (n / b)
case intro.intro.intro
n✝ b n : ℕ
l : List ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
h : digits b (n / b) = l
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ digits b n = n % b :: l
subst h
no goals
case intro.intro.intro
n✝ b n : ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ digits b n = n % b :: digits b (n / b)
exact Nat.digits_def' b2 n0
no goals
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
⊢ 0 < b
linarith
no goals
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ 0 < n
linarith [mul_pos b0 m0]