no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)
simp [h.pow_right n]
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ -[n+1]) (y ^ -[n+1])
simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]