no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ continuants g m = continuants g n
simp only [nth_cont_eq_succ_nth_cont_aux,
  continuantsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminated_at_n]