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
⊢ denominators g m = denominators g n
simp only [denom_eq_conts_b, continuants_stable_of_terminated n_le_m terminated_at_n]