case pos
b w m : ℕ
b_h : b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b

case neg
b w m : ℕ
b_h : ¬b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
b w m : ℕ
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
by_cases b_h : b = 0
case neg
b w m : ℕ
b_h : ¬b = 0
b_pos : 0 < b
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
case neg
b w m : ℕ
b_h : ¬b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
have b_pos := Nat.pos_of_ne_zero b_h
no goals
case pos
b w m : ℕ
b_h : b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
simp [b_h, pow_succ]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b

case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
case neg.h
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
cases' lt_or_ge p (b ^ succ w) with h₁ h₁
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
have h₂ : p / b < b ^ w := by
  rw [div_lt_iff_lt_mul b_pos]
  simpa [pow_succ] using h₁
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p = b * (p / b) + p % b
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
no goals
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p = b * (p / b) + p % b
simp [div_add_mod]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p < b ^ w * b
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p / b < b ^ w
rw [div_lt_iff_lt_mul b_pos]
no goals
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p < b ^ w * b
simpa [pow_succ] using h₁
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
have h₂ : p - b ^ succ w < p :=
  tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _)
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b ^ succ w) / b % b ^ w) + (p - b ^ succ w) % b = b * (p / b % b ^ w) + p % b
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
rw [mod_eq_sub_mod h₁, IH _ h₂]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b ^ succ w) / b % b ^ w) + (p - b ^ succ w) % b = b * (p / b % b ^ w) + p % b
simp only [pow_succ']
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
simp only [GE.ge, pow_succ'] at h₁
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
p_b_ge : b ^ w ≤ p / b
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
have p_b_ge : b ^ w ≤ p / b := by
  rw [le_div_iff_mul_le b_pos, mul_comm]
  exact h₁
no goals
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
p_b_ge : b ^ w ≤ p / b
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * b ^ w ≤ p
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b ^ w ≤ p / b
rw [le_div_iff_mul_le b_pos, mul_comm]
no goals
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * b ^ w ≤ p
exact h₁