K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.get? (of v).s 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.head (of v).s = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
change (of v).s.get? 0 = _
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ (match some (IntFractPair.of (IntFractPair.of v).fr⁻¹), some ∘ fun p => { a := 1, b := ↑p.b } with
    | none, x => none
    | some a, b => b a) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.get? (of v).s 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ (match some (IntFractPair.of (IntFractPair.of v).fr⁻¹), some ∘ fun p => { a := 1, b := ↑p.b } with
    | none, x => none
    | some a, b => b a) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
rfl