case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) Nat.zero = ↑a

case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents' (of ↑a) (Nat.succ n) = ↑a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) n = ↑a
induction' n with n
no goals
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) Nat.zero = ↑a
simp only [zeroth_convergent'_eq_h, of_h_eq_floor, floor_intCast, Nat.zero_eq]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents'Aux (of ↑a).s (Nat.succ n) = 0
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents' (of ↑a) (Nat.succ n) = ↑a
rw [convergents', of_h_eq_floor, floor_intCast, add_right_eq_self]
no goals
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents'Aux (of ↑a).s (Nat.succ n) = 0
exact convergents'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _