English
If the nth element of the simple continued fraction s is gp, then gp.a = 1 and gp.b is an integer (exists z ∈ Z with gp.b = z).
Русский
Если на позиции n частного разложения s получено gp, то gp.a = 1 и gp.b является целым числом (существует z ∈ Z такое, что gp.b = z).
LaTeX
$$$\\\\forall {gp : GenContFract.Pair K} \\\\text{(nth_s_eq)} : (of v).s.get? n = Some gp \\\\Rightarrow gp.a = 1 \\\\land \\\\Exists z : \\\\mathbb{Z}, gp.b = (z : K)$$$
Lean4
/-- Shows that the partial numerators `aᵢ` of the continued fraction are equal to one and the partial
denominators `bᵢ` correspond to integers.
-/
theorem of_partNum_eq_one_and_exists_int_partDen_eq {gp : GenContFract.Pair K} (nth_s_eq : (of v).s.get? n = some gp) :
gp.a = 1 ∧ ∃ z : ℤ, gp.b = (z : K) :=
by
obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _ :=
IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
have : gp = ⟨1, ifp.b⟩ :=
by
have : (of v).s.get? n = some ⟨1, ifp.b⟩ := get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
injection this
simp [this]
