num : Int
den g : Nat
den_nz : den ≠ 0
e : g = Nat.gcd (Int.natAbs num) den
⊢ Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = Nat.gcd (Int.natAbs num) den
⊢ Nat.coprime (Int.natAbs (num / ↑g)) (den / g)
rw [← Int.div_eq_ediv_of_dvd (e ▸ Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
no goals
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = Nat.gcd (Int.natAbs num) den
⊢ Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
exact normalize.reduced den_nz e