α : Type u_1
β : Type ?u.1334
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
α : Type u_1
β : Type ?u.1334
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
rw [add_comm] at hn
no goals
α : Type u_1
β : Type ?u.1334
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
exact hn.left_of_add hm