Lean4
/-- Uses `IntFractPair.stream` to create a sequence with head (i.e. `seq1`) of integer and fractional
parts of a value `v`. The first value of `IntFractPair.stream` is never `none`, so we can safely
extract it and put the tail of the stream in the sequence part.
This is just an intermediate representation and users should not (need to) directly interact with
it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in
`Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean`.
-/
protected def seq1 (v : K) : Stream'.Seq1 <| IntFractPair K :=
⟨IntFractPair.of v, -- the head
-- take the tail of `IntFractPair.stream` since the first element is already in the head
Stream'.Seq.tail
⟨IntFractPair.stream v, -- the underlying stream
stream_isSeq v⟩⟩
-- the proof that the stream is a sequence
