greatestFib_sub_fib_greatestFib_le_greatestFib

English

For n ≠ 0, greatestFib(n - fib(greatestFib(n))) ≤ greatestFib(n) − 2.

Русский

Для n ≠ 0: greatestFib(n - fib(greatestFib(n))) ≤ greatestFib(n) − 2.

LaTeX

$$$$ \forall n,\ (n \neq 0) \Rightarrow \operatorname{greatestFib}(n - \operatorname{fib}(\operatorname{greatestFib}(n))) \le \operatorname{greatestFib}(n) - 2. $$$$

Lean4

theorem greatestFib_sub_fib_greatestFib_le_greatestFib (hn : n ≠ 0) :
    greatestFib (n - fib (greatestFib n)) ≤ greatestFib n - 2 :=
  by
  rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ, succ_pred, ← fib_add_one]
  · exact n.lt_fib_greatestFib_add_one
  · simpa
  · simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

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