case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of { b := b✝, fr := fr✝ }.fr⁻¹)
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_ne_zero : ifp_n.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
cases ifp_n
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ fr✝ = 0 → False
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of { b := b✝, fr := fr✝ }.fr⁻¹)
simp [IntFractPair.stream, stream_nth_eq, nth_fr_ne_zero]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
a✝ : fr✝ = 0
⊢ False
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ fr✝ = 0 → False
intro
no goals
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
a✝ : fr✝ = 0
⊢ False
contradiction