n : Int
d : Nat
z : d ≠ 0
⊢ -mk' (Int.div n ↑(Nat.gcd (Int.natAbs n) d)) (d / Nat.gcd (Int.natAbs n) d) =
    mk' (-Int.div n ↑(Nat.gcd (Int.natAbs n) d)) (d / Nat.gcd (Int.natAbs n) d)
n : Int
d : Nat
z : d ≠ 0
⊢ -normalize n d = normalize (-n) d
simp [normalize, maybeNormalize_eq]
no goals
n : Int
d : Nat
z : d ≠ 0
⊢ -mk' (Int.div n ↑(Nat.gcd (Int.natAbs n) d)) (d / Nat.gcd (Int.natAbs n) d) =
    mk' (-Int.div n ↑(Nat.gcd (Int.natAbs n) d)) (d / Nat.gcd (Int.natAbs n) d)
ext <;> simp [Int.neg_div]