English
The convs' recurrence relation expresses the successor of convs' in terms of floor v and convs' of inverse fractional part.
Русский
Рекуррентность convs' выражает переход к следующему через floor v и convs' от обратной дробной части.
LaTeX
$$$(\operatorname GenContFract.of}(v)).convs'(n+1) = \lfloor v \rfloor.cast + \dfrac{1}{(\operatorname GenContFract.of}(\operatorname{fract}(v)^{-1})).convs'(n)$$$
Lean4
/-- If `a` is an integer, then the `convs'` of its continued fraction expansion
are all equal to `a`.
-/
theorem convs'_of_int (a : ℤ) : (of (a : K)).convs' n = a := by
induction n with
| zero => simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]
| succ =>
rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]
exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _
