no goals
n : Int
d : Nat
⊢ -mkRat n d = mkRat (-n) d
if z : d = 0 then simp [z] else simp [← normalize_eq_mkRat z, neg_normalize]
no goals
n : Int
d : Nat
z : d = 0
⊢ -mkRat n d = mkRat (-n) d
simp [z]
no goals
n : Int
d : Nat
z : ¬d = 0
⊢ -mkRat n d = mkRat (-n) d
simp [← normalize_eq_mkRat z, neg_normalize]