English
If the nth stream equals some p and p.fr ≠ 0, then the (n+1)th stream equals the successor of p, namely the interval inverse of p.fr followed by taking the appropriate IntFractPair component.
Русский
Если поток на позиции n равен некоторому p и p.fr ≠ 0, то следующий член потока равен некоторому объекту, получаемому как обратное дробной части p и преобразование.
LaTeX
$$$\forall p,\; \operatorname{IntFractPair}.\operatorname{stream}(v,n) = \mathrm{Some}(p) \land p.f r \neq 0 \Rightarrow \operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \mathrm{Some}(\operatorname{IntFractPair}.\operatorname{of}(p.f r^{-1}))$$$
Lean4
/-- An easier to use version of one direction of
`GenContFract.IntFractPair.succ_nth_stream_eq_some_iff`. -/
theorem stream_succ_of_some {p : IntFractPair K} (h : IntFractPair.stream v n = some p) (h' : p.fr ≠ 0) :
IntFractPair.stream v (n + 1) = some (IntFractPair.of p.fr⁻¹) :=
succ_nth_stream_eq_some_iff.mpr ⟨p, h, h', rfl⟩
