rw [Cycle.chain_iff_pairwise] at hl
l : Cycle ℤ
x y : ℤ
hl : Cycle.Chain (fun x x_1 => x ∣ x_1) l
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs
l : Cycle ℤ
x y : ℤ
hl : ∀ a ∈ l, ∀ b ∈ l, a ∣ b
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs