Lean4
/-- A *simple continued fraction* (scf) is a generalized continued fraction (gcf) whose partial
numerators are equal to one.
$$
h + \dfrac{1}
{b_0 + \dfrac{1}
{b_1 + \dfrac{1}
{b_2 + \dfrac{1}
{b_3 + \dots}}}}
$$
For convenience, one often writes `[h; b₀, b₁, b₂,...]`.
It is encoded as the subtype of gcfs that satisfy `GenContFract.IsSimpContFract`.
-/
def SimpContFract [One α] :=
{ g : GenContFract α // g.IsSimpContFract }
-- Interlude: define some expected coercions.