English
If a is an integer, then convs' n equals a cast for all n.
Русский
Если a — целое, convs' n = a.cast для всех n.
LaTeX
$$$\forall n,\; (\operatorname GenContFract.of a.cast).convs' n = a.cast$$$
Lean4
/-- Recurrence for the `GenContFract.of` an element `v` of `K` in terms of that of the inverse of
the fractional part of `v`.
-/
theorem of_s_succ (n : ℕ) : (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n :=
by
rcases eq_or_ne (fract v) 0 with h | h
· obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int, Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]
rcases eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ | h₁
·
rwa [h₁, ← terminatedAt_iff_s_none, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]
· obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp h₁
obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp
have Hp := get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁
rw [← stream_succ h] at hp'₁
rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]
