no goals
num den : Int
⊢ -num /. -den = num /. den
match den with
| Nat.succ n => simp [divInt, Int.neg_ofNat_succ, normalize_eq_mkRat, Int.neg_neg]
| 0 => rfl
| Int.negSucc n => simp [divInt, Int.neg_negSucc, normalize_eq_mkRat, Int.neg_neg]
no goals
num den : Int
n : Nat
⊢ -num /. -↑(Nat.succ n) = num /. ↑(Nat.succ n)
simp [divInt, Int.neg_ofNat_succ, normalize_eq_mkRat, Int.neg_neg]
no goals
num den : Int
⊢ -num /. -0 = num /. 0
rfl
no goals
num den : Int
n : Nat
⊢ -num /. -Int.negSucc n = num /. Int.negSucc n
simp [divInt, Int.neg_negSucc, normalize_eq_mkRat, Int.neg_neg]