English
The tail of the s-sequence after a succ step corresponds to the inverse fractional part, i.e., (of v).s.get? (n+1) = (of (fract v)^{-1}).s.get? n.
Русский
Хвост последовательности s после шага succ равен последовательности от обратной дробной части: (of v).s.get? (n+1) = (of (fract v)^{-1}).s.get? n.
LaTeX
$$$\forall n,\; (\operatorname GenContFract.of}(v)).s.get? (n+1) = (\operatorname GenContFract.of}(\operatorname{fract}(v)^{-1})).s.get? n$$$
Lean4
/-- The recurrence relation for the `convs'` of the continued fraction expansion
of an element `v` of `K` in terms of the convergents of the inverse of its fractional part.
-/
theorem convs'_succ : (of v).convs' (n + 1) = ⌊v⌋ + 1 / (of (fract v)⁻¹).convs' 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 [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero, div_zero, add_zero,
floor_intCast]
· rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]
exact congr_arg (1 / ·) (by rw [convs', of_h_eq_floor, add_right_inj, of_s_tail])
