case a
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
⊢ Stream'.nth (convergents ↑↑c) n = Stream'.nth (convergents' ↑↑c) n
K : Type u_1
n : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
⊢ convergents ↑↑c = convergents' ↑↑c
ext n
case a.s_pos
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? (↑↑c).s m = some gp → 0 < gp.a ∧ 0 < gp.b
case a
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
⊢ Stream'.nth (convergents ↑↑c) n = Stream'.nth (convergents' ↑↑c) n
apply convergents_eq_convergents'
case a.s_pos
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : Stream'.Seq.get? (↑↑c).s m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b
case a.s_pos
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? (↑↑c).s m = some gp → 0 < gp.a ∧ 0 < gp.b
intro gp m _ s_nth_eq
no goals
case a.s_pos
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : Stream'.Seq.get? (↑↑c).s m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b
exact ⟨zero_lt_one.trans_le ((c : SimpleContinuedFraction K).property m gp.a
  (part_num_eq_s_a s_nth_eq)).symm.le, c.property m gp.b <| part_denom_eq_s_b s_nth_eq⟩