[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Decidable (TerminatedAt g n)
[PROOFSTEP]
unfold TerminatedAt
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Decidable (Stream'.Seq.TerminatedAt g.s n)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : One α
a : α
n : ℕ
aₙ : α
h : Stream'.Seq.get? (partialNumerators (GeneralizedContinuedFraction.ofInteger a)) n = some aₙ
⊢ aₙ = 1
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
inst✝² : One α
inst✝¹ : Zero α
inst✝ : LT α
a : α
n : ℕ
bₙ : α
h : Stream'.Seq.get? (partialDenominators ↑(SimpleContinuedFraction.ofInteger a)) n = some bₙ
⊢ 0 < bₙ
[PROOFSTEP]
cases h
