no goals
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = Nat.gcd (Int.natAbs num) den
⊢ Int.natAbs (Int.div num ↑g) = Int.natAbs num / g
match num, num.eq_nat_or_neg with
| _, ⟨_, .inl rfl⟩ => rfl
| _, ⟨_, .inr rfl⟩ => rw [Int.neg_div, Int.natAbs_neg, Int.natAbs_neg]; rfl
no goals
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = Nat.gcd (Int.natAbs ↑w✝) den
⊢ Int.natAbs (Int.div ↑w✝ ↑g) = Int.natAbs ↑w✝ / g
rfl
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = Nat.gcd (Int.natAbs (-↑w✝)) den
⊢ Int.natAbs (Int.div ↑w✝ ↑g) = Int.natAbs ↑w✝ / g
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = Nat.gcd (Int.natAbs (-↑w✝)) den
⊢ Int.natAbs (Int.div (-↑w✝) ↑g) = Int.natAbs (-↑w✝) / g
rw [Int.neg_div, Int.natAbs_neg, Int.natAbs_neg]
no goals
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = Nat.gcd (Int.natAbs (-↑w✝)) den
⊢ Int.natAbs (Int.div ↑w✝ ↑g) = Int.natAbs ↑w✝ / g
rfl