case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m✝ n✝ m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹

case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
obtain rfl | ha := eq_or_ne a 0
no goals
case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m✝ n✝ m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹
rw [zero_pow (tsub_pos_of_lt h), zero_pow (n.zero_le.trans_lt h), zero_mul]
no goals
case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
exact pow_sub₀ _ ha h.le