squashSeq_nth_of_not_terminated — Mathlib

English

If m < n, then the m-th component of squashGCF g (n+1) equals the m-th component of g.

Русский

Если m < n, то m-ая компонентa squashGCF g (n+1) совпадает с m-ой компонентой g.

LaTeX

$$(squashGCF(g,(n+1))).s.get? m = g.s.get? m, for m < n.$$

Lean4

/-- If the sequence has not terminated before position `n + 1`, the value at `n + 1` gets
squashed into position `n`. -/
theorem squashSeq_nth_of_not_terminated {gp_n gp_succ_n : Pair K} (s_nth_eq : s.get? n = some gp_n)
    (s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n) :
    (squashSeq s n).get? n = some ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ := by simp [*, squashSeq]

Похожие утверждения