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