case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v = 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n

case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
cases' eq_or_ne (fract v) 0 with h h
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ convergents' (of ↑a) (n + 1) = ↑⌊↑a⌋ + 1 / convergents' (of (fract ↑a)⁻¹) n
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v = 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
no goals
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ convergents' (of ↑a) (n + 1) = ↑⌊↑a⌋ + 1 / convergents' (of (fract ↑a)⁻¹) n
rw [convergents'_of_int, fract_intCast, inv_zero, ← cast_zero, convergents'_of_int, cast_zero,
  div_zero, add_zero, floor_intCast]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.a /
      ({ a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convergents'Aux (Stream'.Seq.tail (of v).s) n) =
    1 / convergents' (of (fract v)⁻¹) n
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
rw [convergents', of_h_eq_floor, add_right_inj, convergents'Aux_succ_some (of_s_head h)]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convergents'Aux (Stream'.Seq.tail (of v).s) n = convergents' (of (fract v)⁻¹) n
rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail]