eq_of_xn_modEq_lem2 — Mathlib

English

Suppose 2·xn(a1, n) = xn(a1, n+1). Then a = 2 and n = 0.

Русский

Пусть 2·xn(a1, n) = xn(a1, n+1). Тогда a = 2 и n = 0.

LaTeX

$$$$ 2 \\cdot xn(a1, n) = xn(a1, n+1) \\implies a = 2 \\text{ и } n = 0 $$$$

Lean4

theorem eq_of_xn_modEq_lem2 {n} (h : 2 * xn a1 n = xn a1 (n + 1)) : a = 2 ∧ n = 0 :=
  by
  rw [xn_succ, mul_comm] at h
  have : n = 0 :=
    n.eq_zero_or_pos.resolve_right fun np =>
      _root_.ne_of_lt
        (lt_of_le_of_lt (Nat.mul_le_mul_left _ a1) (Nat.lt_add_of_pos_right <| mul_pos (d_pos a1) (strictMono_y a1 np)))
        h
  cases this; simp at h; exact ⟨h.symm, rfl⟩

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