Theorem: Imo2006P5.Int.natAbs_eq_of_chain_dvd (Compfiles/Imo2006P5.lean)

State before:
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
Tactic:
rw [Cycle.chain_iff_pairwise] at hl
State after:
l : Cycle ℤ
x y : ℤ
hl : ∀ a ∈ l, ∀ b ∈ l, a ∣ b
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs

State before:
l : Cycle ℤ
x y : ℤ
hl : ∀ a ∈ l, ∀ b ∈ l, a ∣ b
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs
Tactic:
exact Int.natAbs_eq_of_dvd_dvd (hl x hx y hy) (hl y hy x hx)
State after:
no goals