decode_ge_two — Mathlib

English

If 2 ≤ n, then decode n = none.

Русский

Если 2 ≤ n, то decode n = none.

LaTeX

$$$ \forall n:\mathbb{N},\ 2 \le n \Rightarrow \mathrm{decode}(n) = \mathrm{none}$$$

Lean4

theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none :=
  by
  suffices decodeSum n = none by
    change (decodeSum n).bind _ = none
    rw [this]
    rfl
  have : 1 ≤ n / 2 := by
    rw [Nat.le_div_iff_mul_le]
    exacts [h, by decide]
  obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)
  simp only [decodeSum, boddDiv2_eq, div2_val]; cases bodd n <;> simp [e]

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