α : Type ?u.244728
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)
α : Type ?u.244728
k n m : ℕ
H : Raised n m
⊢ Raised (n + k) (m + k)
rw [add_comm, add_comm m]
no goals
α : Type ?u.244728
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)
exact H.add_left _