K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ (m : ℕ), m < n_1 → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m) →
      n_1 ≤ n → continuantsAux g n_1 = continuantsAux (squashGCF g n) n_1
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
⊢ ∀ (n_1 : ℕ),
    (∀ (m : ℕ), m < n_1 → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m) →
      n_1 ≤ n → continuantsAux g n_1 = continuantsAux (squashGCF g n) n_1
clear m
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
IH : ∀ (m_1 : ℕ), m_1 < m → m_1 ≤ n → continuantsAux g m_1 = continuantsAux (squashGCF g n) m_1
m_le_n : m ≤ n
⊢ continuantsAux g m = continuantsAux (squashGCF g n) m
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ (m : ℕ), m < n_1 → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m) →
      n_1 ≤ n → continuantsAux g n_1 = continuantsAux (squashGCF g n) n_1
intro m IH m_le_n
case zero
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
IH : ∀ (m : ℕ), m < Nat.zero → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m
m_le_n : Nat.zero ≤ n
⊢ continuantsAux g Nat.zero = continuantsAux (squashGCF g n) Nat.zero

case succ
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m
m_le_n : Nat.succ m' ≤ n
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g n) (Nat.succ m')
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
IH : ∀ (m_1 : ℕ), m_1 < m → m_1 ≤ n → continuantsAux g m_1 = continuantsAux (squashGCF g n) m_1
m_le_n : m ≤ n
⊢ continuantsAux g m = continuantsAux (squashGCF g n) m
cases' m with m'
no goals
case zero
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
IH : ∀ (m : ℕ), m < Nat.zero → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m
m_le_n : Nat.zero ≤ n
⊢ continuantsAux g Nat.zero = continuantsAux (squashGCF g n) Nat.zero
rfl
case succ.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ Nat.zero → continuantsAux g m = continuantsAux (squashGCF g Nat.zero) m
m_le_n : Nat.succ m' ≤ Nat.zero
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g Nat.zero) (Nat.succ m')

case succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ m' ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ m')
case succ
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m
m_le_n : Nat.succ m' ≤ n
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g n) (Nat.succ m')
cases' n with n'
no goals
case succ.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ Nat.zero → continuantsAux g m = continuantsAux (squashGCF g Nat.zero) m
m_le_n : Nat.succ m' ≤ Nat.zero
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g Nat.zero) (Nat.succ m')
exact (m'.not_succ_le_zero m_le_n).elim
case succ.succ.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' : ℕ
IH :
  ∀ (m : ℕ), m < Nat.succ Nat.zero → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ Nat.zero ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ Nat.zero) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ Nat.zero)

case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
case succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ m' ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ m')
cases' m' with m''
no goals
case succ.succ.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' : ℕ
IH :
  ∀ (m : ℕ), m < Nat.succ Nat.zero → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ Nat.zero ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ Nat.zero) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ Nat.zero)
rfl
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
have succ_m''th_conts_aux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this : m'' < m'' + 2
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this : m'' < m'' + 2
m''th_conts_aux_eq : continuantsAux g m'' = continuantsAux (squashGCF g (Nat.succ n')) m''
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this : m'' < m'' + 2
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
have m''th_conts_aux_eq := IH m'' this (le_trans this.le m_le_n)
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this✝ : m'' < m'' + 2
m''th_conts_aux_eq : continuantsAux g m'' = continuantsAux (squashGCF g (Nat.succ n')) m''
this : Stream'.Seq.get? (squashGCF g (n' + 1)).s m'' = Stream'.Seq.get? g.s m''
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this : m'' < m'' + 2
m''th_conts_aux_eq : continuantsAux g m'' = continuantsAux (squashGCF g (Nat.succ n')) m''
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' :=
  squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
no goals
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this✝ : m'' < m'' + 2
m''th_conts_aux_eq : continuantsAux g m'' = continuantsAux (squashGCF g (Nat.succ n')) m''
this : Stream'.Seq.get? (squashGCF g (n' + 1)).s m'' = Stream'.Seq.get? g.s m''
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
simp [continuantsAux, succ_m''th_conts_aux_eq, m''th_conts_aux_eq, this]