a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ b = 0
a b : ℤ
w : a ∣ b
h : natAbs b < natAbs a
⊢ b = 0
rw [← natAbs_dvd, ← dvd_natAbs, coe_nat_dvd] at w
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ natAbs b = 0
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ b = 0
rw [← natAbs_eq_zero]
no goals
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ natAbs b = 0
exact eq_zero_of_dvd_of_lt w h