a b c : ℚ
⊢ (match -1, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    -1
a b c : ℚ
⊢ -1 /. 1 = -1
rw [divInt]
a b c : ℚ
⊢ mkRat (-1) 1 = -1
a b c : ℚ
⊢ (match -1, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    -1
simp
no goals
a b c : ℚ
⊢ mkRat (-1) 1 = -1
rfl