K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
let g := of v
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v Nat.zero = some ifp_n →
      v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) ifp_n.fr

case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v (Nat.succ n) = some ifp_n →
      v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_n.fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
induction' n with n IH
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) ifp_zero.fr
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v Nat.zero = some ifp_n →
      v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) ifp_n.fr
intro ifp_zero stream_zero_eq
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
this : IntFractPair.of v = ifp_zero
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) ifp_zero.fr
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) ifp_zero.fr
have : IntFractPair.of v = ifp_zero := by
  have : IntFractPair.stream v 0 = some (IntFractPair.of v) := rfl
  simpa only [Nat.zero_eq, this, Option.some.injEq] using stream_zero_eq
case zero.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
this : IntFractPair.of v = ifp_zero
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) ifp_zero.fr
cases this
case zero.refl.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr

case zero.refl.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_ne_zero : ¬Int.fract v = 0
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr
case zero.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr
cases' Decidable.em (Int.fract v = 0) with fract_eq_zero fract_ne_zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
this : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ IntFractPair.of v = ifp_zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
⊢ IntFractPair.of v = ifp_zero
have : IntFractPair.stream v 0 = some (IntFractPair.of v) := rfl
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v Nat.zero = some ifp_zero
this : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ IntFractPair.of v = ifp_zero
simpa only [Nat.zero_eq, this, Option.some.injEq] using stream_zero_eq
case zero.refl.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = ↑⌊v⌋
case zero.refl.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr
suffices v = ⌊v⌋ by
  field_simp [nextContinuants, nextNumerator, nextDenominator, compExactValue]
  have : (IntFractPair.of v).fr = Int.fract v := rfl
  rwa [this, if_pos fract_eq_zero]
no goals
case zero.refl.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = ↑⌊v⌋
calc
  v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
  _ = ⌊v⌋ := by simp [fract_eq_zero]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
this : v = ↑⌊v⌋
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
this : v = ↑⌊v⌋
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr
field_simp [nextContinuants, nextNumerator, nextDenominator, compExactValue]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
this✝ : v = ↑⌊v⌋
this : (IntFractPair.of v).fr = Int.fract v
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
this : v = ↑⌊v⌋
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
have : (IntFractPair.of v).fr = Int.fract v := rfl
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
this✝ : v = ↑⌊v⌋
this : (IntFractPair.of v).fr = Int.fract v
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
rwa [this, if_pos fract_eq_zero]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = Int.fract v + ↑⌊v⌋
rw [Int.fract_add_floor]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ Int.fract v + ↑⌊v⌋ = ↑⌊v⌋
simp [fract_eq_zero]
case zero.refl.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_ne_zero : ¬Int.fract v = 0
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
case zero.refl.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_ne_zero : ¬Int.fract v = 0
⊢ v = compExactValue (continuantsAux (of v) Nat.zero) (continuantsAux (of v) (Nat.zero + 1)) (IntFractPair.of v).fr
field_simp [continuantsAux, nextContinuants, nextNumerator, nextDenominator,
  of_h_eq_floor, compExactValue]
case zero.refl.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_ne_zero : ¬Int.fract v = 0
this : (IntFractPair.of v).fr = Int.fract v
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
case zero.refl.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_ne_zero : ¬Int.fract v = 0
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
have : (IntFractPair.of v).fr = Int.fract v := rfl
no goals
case zero.refl.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
stream_zero_eq : IntFractPair.stream v Nat.zero = some (IntFractPair.of v)
fract_ne_zero : ¬Int.fract v = 0
this : (IntFractPair.of v).fr = Int.fract v
⊢ v = if (IntFractPair.of v).fr = 0 then ↑⌊v⌋ else ↑⌊v⌋ + (IntFractPair.of v).fr
rw [this, if_neg fract_ne_zero, Int.floor_add_fract]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v (Nat.succ n) = some ifp_n →
      v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_n.fr
intro ifp_succ_n succ_nth_stream_eq
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
obtain ⟨ifp_n, nth_stream_eq, nth_fract_ne_zero, -⟩ :
  ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
    ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
let conts := g.continuantsAux (n + 2)
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue (continuantsAux (of v) n) pconts ifp_n.fr
pconts_eq : pconts = continuantsAux g (n + 1)
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n →
      v = compExactValue (continuantsAux (of v) n) (continuantsAux (of v) (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
⊢ v = compExactValue (continuantsAux (of v) (Nat.succ n)) (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
set pconts := g.continuantsAux (n + 1) with pconts_eq
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue (continuantsAux (of v) n) pconts ifp_n.fr
pconts_eq : pconts = continuantsAux g (n + 1)
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
set ppconts := g.continuantsAux n with ppconts_eq
case succ.intro.intro.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr

case succ.intro.intro.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
case succ.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
cases' Decidable.em (ifp_succ_n.fr = 0) with ifp_succ_n_fr_eq_zero ifp_succ_n_fr_ne_zero
case succ.intro.intro.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ v = conts.a / conts.b
case succ.intro.intro.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

case succ.intro.intro.intro.inl.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ v = conts.a / conts.b
case succ.intro.intro.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ v = conts.a / conts.b
obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor⟩ :
  ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋
case succ.intro.intro.intro.inl.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ v = conts.a / conts.b
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

case succ.intro.intro.intro.inl.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ v = conts.a / conts.b
exact IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero
case succ.intro.intro.intro.inl.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
this : ifp_n' = ifp_n
⊢ v = conts.a / conts.b
case succ.intro.intro.intro.inl.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ v = conts.a / conts.b
have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
⊢ v = conts.a / conts.b
case succ.intro.intro.intro.inl.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
this : ifp_n' = ifp_n
⊢ v = conts.a / conts.b
cases this
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ v = conts.a / conts.b
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
⊢ v = conts.a / conts.b
have s_nth_eq : g.s.get? n = some ⟨1, ⌊ifp_n.fr⁻¹⌋⟩ :=
  get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero nth_stream_eq nth_fract_ne_zero
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ifp_n.fr⁻¹ }
⊢ v = conts.a / conts.b
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ v = conts.a / conts.b
rw [← ifp_n_fract_inv_eq_floor] at s_nth_eq
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ifp_n.fr⁻¹ }
⊢ v = compExactValue ppconts pconts ifp_n.fr
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ifp_n.fr⁻¹ }
⊢ v = conts.a / conts.b
suffices v = compExactValue ppconts pconts ifp_n.fr by
  simpa [continuantsAux, s_nth_eq, compExactValue, nth_fract_ne_zero] using this
no goals
case succ.intro.intro.intro.inl.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ifp_n.fr⁻¹ }
⊢ v = compExactValue ppconts pconts ifp_n.fr
exact IH nth_stream_eq
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
this : v = conts.a / conts.b
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
simpa [compExactValue, ifp_succ_n_fr_eq_zero]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ ifp_n' = ifp_n
injection Eq.trans nth_stream_eq'.symm nth_stream_eq
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ifp_n.fr⁻¹ }
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ v = conts.a / conts.b
simpa [continuantsAux, s_nth_eq, compExactValue, nth_fract_ne_zero] using this
case succ.intro.intro.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
case succ.intro.intro.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
suffices
  compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr by
  have : v = compExactValue ppconts pconts ifp_n.fr := IH nth_stream_eq
  conv_lhs => rw [this]
  assumption
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

case succ.intro.intro.intro.inr.intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
case succ.intro.intro.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_ne_zero, ⟨refl⟩⟩ :
  ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
    ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
case succ.intro.intro.intro.inr.intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

case succ.intro.intro.intro.inr.intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
case succ.intro.intro.intro.inr.intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
this : ifp_n' = ifp_n
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
this : ifp_n' = ifp_n
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
cases this
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have s_nth_eq : g.s.get? n = some ⟨1, (⌊ifp_n.fr⁻¹⌋ : K)⟩ :=
  get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero nth_stream_eq ifp_n_fract_ne_zero
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
let ppA := ppconts.a
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
let ppB := ppconts.b
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
let pA := pconts.a
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
let pB := pconts.b
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have : compExactValue ppconts pconts ifp_n.fr =
    (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) := by
  field_simp [ifp_n_fract_ne_zero, compExactValue, nextContinuants, nextNumerator,
    nextDenominator]
  ac_rfl
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
rw [this]
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have tmp_calc :=
  compExactValue_correctness_of_stream_eq_some_aux_comp pA ppA ifp_succ_n_fr_ne_zero
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have tmp_calc' :=
  compExactValue_correctness_of_stream_eq_some_aux_comp pB ppB ifp_succ_n_fr_ne_zero
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
let f := Int.fract (1 / ifp_n.fr)
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have f_ne_zero : f ≠ 0 := by simpa using ifp_succ_n_fr_ne_zero
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
rw [inv_eq_one_div] at tmp_calc tmp_calc'
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have hA : (↑⌊1 / ifp_n.fr⌋ * pA + ppA) + pA * f = pA * (1 / ifp_n.fr) + ppA := by
  have := congrFun (congrArg HMul.hMul tmp_calc) f
  rwa [right_distrib, div_mul_cancel (h := f_ne_zero),
    div_mul_cancel (h := f_ne_zero)] at this
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have hB : (↑⌊1 / ifp_n.fr⌋ * pB + ppB) + pB * f = pB * (1 / ifp_n.fr) + ppB := by
  have := congrFun (congrArg HMul.hMul tmp_calc') f
  rwa [right_distrib, div_mul_cancel (h := f_ne_zero),
    div_mul_cancel (h := f_ne_zero)] at this
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    if (IntFractPair.of (1 / ifp_n.fr)).fr = 0 then
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b)
    else
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
          (continuantsAux (of v) (n + 1)).a * (IntFractPair.of (1 / ifp_n.fr)).fr) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
          (continuantsAux (of v) (n + 1)).b * (IntFractPair.of (1 / ifp_n.fr)).fr)
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
field_simp [compExactValue, continuantsAux_recurrence s_nth_eq ppconts_eq pconts_eq,
  nextContinuants, nextNumerator, nextDenominator]
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    if (IntFractPair.of (1 / ifp_n.fr)).fr = 0 then
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b)
    else
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
          (continuantsAux (of v) (n + 1)).a * (IntFractPair.of (1 / ifp_n.fr)).fr) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
          (continuantsAux (of v) (n + 1)).b * (IntFractPair.of (1 / ifp_n.fr)).fr)
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    if (IntFractPair.of (1 / ifp_n.fr)).fr = 0 then
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b)
    else
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
          (continuantsAux (of v) (n + 1)).a * (IntFractPair.of (1 / ifp_n.fr)).fr) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
          (continuantsAux (of v) (n + 1)).b * (IntFractPair.of (1 / ifp_n.fr)).fr)
have hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f := rfl
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
        (continuantsAux (of v) (n + 1)).a * f) /
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
        (continuantsAux (of v) (n + 1)).b * f)

K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    if (IntFractPair.of (1 / ifp_n.fr)).fr = 0 then
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b)
    else
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
          (continuantsAux (of v) (n + 1)).a * (IntFractPair.of (1 / ifp_n.fr)).fr) /
        (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
          (continuantsAux (of v) (n + 1)).b * (IntFractPair.of (1 / ifp_n.fr)).fr)
rw [one_div, if_neg _, ← one_div, hfr]
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    ((continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a * ifp_n.fr) /
      ((continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b * ifp_n.fr)

K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
        (continuantsAux (of v) (n + 1)).a * f) /
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
        (continuantsAux (of v) (n + 1)).b * f)

K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
field_simp [hA, hB]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
    ((continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a * ifp_n.fr) /
      ((continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b * ifp_n.fr)

K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
ac_rfl
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
rwa [inv_eq_one_div, hfr]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
this✝ : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
this : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
have : v = compExactValue ppconts pconts ifp_n.fr := IH nth_stream_eq
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
this✝ : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
this✝ : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ v = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
conv_lhs => rw [this]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_succ_n_fr_ne_zero : ¬ifp_succ_n.fr = 0
this✝ : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts (continuantsAux (of v) (Nat.succ n + 1)) ifp_succ_n.fr
assumption
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n'.fr⁻¹).fr = 0
⊢ ifp_n' = ifp_n
injection Eq.trans nth_stream_eq'.symm nth_stream_eq
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ ((continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a * ifp_n.fr) /
      ((continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b * ifp_n.fr) =
    ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b)
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
field_simp [ifp_n_fract_ne_zero, compExactValue, nextContinuants, nextNumerator,
  nextDenominator]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ ((continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a * ifp_n.fr) /
      ((continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b * ifp_n.fr) =
    ((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
      ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b)
ac_rfl
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
⊢ f ≠ 0
simpa using ifp_succ_n_fr_ne_zero
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this✝ : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
this :
  ((↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA) * f =
    (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr) * f
⊢ ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
⊢ ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
have := congrFun (congrArg HMul.hMul tmp_calc) f
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this✝ : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
this :
  ((↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA) * f =
    (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr) * f
⊢ ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
rwa [right_distrib, div_mul_cancel (h := f_ne_zero),
  div_mul_cancel (h := f_ne_zero)] at this
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this✝ : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
this :
  ((↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB) * f =
    (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr) * f
⊢ ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
⊢ ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
have := congrFun (congrArg HMul.hMul tmp_calc') f
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GeneralizedContinuedFraction K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := continuantsAux g (n + 2)
pconts : Pair K := continuantsAux g (n + 1)
pconts_eq : pconts = continuantsAux g (n + 1)
ppconts : Pair K := continuantsAux g n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = continuantsAux g n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (Nat.succ n) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0
s_nth_eq : Stream'.Seq.get? g.s n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this✝ : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
this :
  ((↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB) * f =
    (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr) * f
⊢ ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
rwa [right_distrib, div_mul_cancel (h := f_ne_zero),
  div_mul_cancel (h := f_ne_zero)] at this