no goals
M✝ : Type ?u.81771
N : Type ?u.81774
P : Type ?u.81777
M : Type u_1
inst✝ : Monoid M
c : Con M
w x : M
x✝ : ↑c w x
⊢ ↑c (w ^ 0) (x ^ 0)
simpa using c.refl _
no goals
M✝ : Type ?u.81771
N : Type ?u.81774
P : Type ?u.81777
M : Type u_1
inst✝ : Monoid M
c : Con M
n : ℕ
w x : M
h : ↑c w x
⊢ ↑c (w ^ Nat.succ n) (x ^ Nat.succ n)
simpa [pow_succ] using c.mul h (Con.pow c n h)