no goals
M : Type u_1
N : Type ?u.99934
P : Type ?u.99937
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
n : ℕ
w x : M
h : ↑c w x
⊢ ↑c (w ^ Int.ofNat n) (x ^ Int.ofNat n)
simpa only [zpow_ofNat, Int.ofNat_eq_coe] using c.pow n h
no goals
M : Type u_1
N : Type ?u.99934
P : Type ?u.99937
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
n : ℕ
w x : M
h : ↑c w x
⊢ ↑c (w ^ Int.negSucc n) (x ^ Int.negSucc n)
simpa only [zpow_negSucc] using c.inv (c.pow _ h)