no goals
⊢ ↑(0 / 0) = ↑0 / ↑0
simp [Int.ediv_zero]
n d : PosNum
⊢ ↑↑(PosNum.div' n d) = ↑(pos n) / ↑(pos d)
n d : PosNum
⊢ ↑(PosNum.div' n d) = ↑(pos n) / ↑(pos d)
rw [← Num.to_nat_to_int]
no goals
n d : PosNum
⊢ ↑↑(PosNum.div' n d) = ↑(pos n) / ↑(pos d)
simp
n d : PosNum
⊢ -↑↑(PosNum.div' n d) = ↑(pos n) / ↑(neg d)
n d : PosNum
⊢ -↑(PosNum.div' n d) = ↑(pos n) / ↑(neg d)
rw [← Num.to_nat_to_int]
no goals
n d : PosNum
⊢ -↑↑(PosNum.div' n d) = ↑(pos n) / ↑(neg d)
simp
n d : PosNum
⊢ -↑(↑(PosNum.pred' n) / ↑(Num.pos d) + 1) = -(↑↑(PosNum.pred' n) + 1) / (↑↑(PosNum.pred' d) + 1)
n d : PosNum
⊢ -↑(Num.succ' (PosNum.pred' n / Num.pos d)) = -↑n / ↑d
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
  Num.div_to_nat]
n d : PosNum
⊢ -[↑(PosNum.pred' n) / ↑d+1] = -[↑(PosNum.pred' n) / (↑(PosNum.pred' d) + 1)+1]
n d : PosNum
⊢ -↑(↑(PosNum.pred' n) / ↑(Num.pos d) + 1) = -(↑↑(PosNum.pred' n) + 1) / (↑↑(PosNum.pred' d) + 1)
change -[n.pred' / ↑d+1] = -[n.pred' / (d.pred' + 1)+1]
no goals
n d : PosNum
⊢ -[↑(PosNum.pred' n) / ↑d+1] = -[↑(PosNum.pred' n) / (↑(PosNum.pred' d) + 1)+1]
rw [d.to_nat_eq_succ_pred]
n d : PosNum
⊢ ↑(↑(PosNum.pred' n) / ↑(Num.pos d) + 1) = -(↑↑(PosNum.pred' n) + 1) / -(↑↑(PosNum.pred' d) + 1)
n d : PosNum
⊢ ↑(Num.succ' (PosNum.pred' n / Num.pos d)) = -↑n / -↑d
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
  Num.div_to_nat]
n d : PosNum
⊢ ↑(Nat.succ (↑(PosNum.pred' n) / ↑d)) = ↑(Nat.succ (↑(PosNum.pred' n) / (↑(PosNum.pred' d) + 1)))
n d : PosNum
⊢ ↑(↑(PosNum.pred' n) / ↑(Num.pos d) + 1) = -(↑↑(PosNum.pred' n) + 1) / -(↑↑(PosNum.pred' d) + 1)
change (Nat.succ (_ / d) : ℤ) = Nat.succ (n.pred' / (d.pred' + 1))
no goals
n d : PosNum
⊢ ↑(Nat.succ (↑(PosNum.pred' n) / ↑d)) = ↑(Nat.succ (↑(PosNum.pred' n) / (↑(PosNum.pred' d) + 1)))
rw [d.to_nat_eq_succ_pred]