contsAux_eq_contsAux_squashGCF_of_le

English

For any m ≤ n, contsAux g m equals contsAux (squashGCF g n) m.

Русский

Для любого m ≤ n contsAux g m равно contsAux (squashGCF g n) m.

LaTeX

$$$$\text{contsAux}(g,m) = \text{contsAux}(\text{squashGCF}(g,n),m) \quad (m \le n).$$$$

Lean4

/-- The auxiliary continuants before the squashed position stay the same. -/
theorem contsAux_eq_contsAux_squashGCF_of_le {m : ℕ} : m ≤ n → contsAux g m = (squashGCF g n).contsAux m :=
  Nat.strong_induction_on m
    (by
      clear m
      intro m IH m_le_n
      rcases m with - | m'
      · rfl
      · rcases n with - | n'
        · exact (m'.not_succ_le_zero m_le_n).elim
        · rcases m' with - | m''
          · rfl
          · -- get some inequalities to instantiate the IH for m'' and m'' + 1

            have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
            have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
            have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
            have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)
            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)
            simp [contsAux, succ_m''th_contsAux_eq, m''th_contsAux_eq, this])

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