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