a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ ↑(natAbs a) ∣ ↑(natAbs b) → ↑(natAbs b) ∣ ↑(natAbs a) → ↑(natAbs a) = ↑(natAbs b)
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ a ∣ b → b ∣ a → a = b
rw [← natAbs_of_nonneg H1, ← natAbs_of_nonneg H2]
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ natAbs a ∣ natAbs b → natAbs b ∣ natAbs a → natAbs a = natAbs b
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ ↑(natAbs a) ∣ ↑(natAbs b) → ↑(natAbs b) ∣ ↑(natAbs a) → ↑(natAbs a) = ↑(natAbs b)
rw [ofNat_dvd, ofNat_dvd, ofNat_inj]
no goals
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ natAbs a ∣ natAbs b → natAbs b ∣ natAbs a → natAbs a = natAbs b
apply Nat.dvd_antisymm