greatestFib_fib — Mathlib

English

If a,b,c ∈ ℕ with b+2 ≤ a and c+2 ≤ b, then c+4 ≤ a.

Русский

Пусть a,b,c ∈ ℕ с b+2 ≤ a и c+2 ≤ b; тогда c+4 ≤ a.

LaTeX

$$$$ \forall a,b,c \in \mathbb{N},\ (b+2 \le a) \land (c+2 \le b) \Rightarrow (c+4 \le a). $$$$

Lean4

@[simp]
theorem greatestFib_fib : ∀ {n}, n ≠ 1 → greatestFib (fib n) = n
  | 0, _ => rfl
  | _n + 2, _ =>
    findGreatest_eq_iff.2 ⟨le_fib_add_one _, fun _ ↦ le_rfl, fun _m hnm _ ↦ ((fib_lt_fib le_add_self).2 hnm).not_ge⟩

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