G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have h1 : m - n + n = m := tsub_add_cancel_of_le h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m
rw [← pow_add, h1]