no goals
α : Type u_1
β : Type ?u.29967
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ Cycle.length (periodicOrbit f x) = minimalPeriod f x
rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]