addLeftMono — Mathlib

English

For any a, it is not the case that a < 0 in WithZero α.

Русский

Для любого a неверно, что a < 0 в WithZero α.

LaTeX

$$$ \neg (a < 0) $$$

Lean4

protected theorem addLeftMono [AddZeroClass α] [AddLeftMono α] (h : ∀ a : α, 0 ≤ a) : AddLeftMono (WithZero α) :=
  by
  refine ⟨fun a b c hbc => ?_⟩
  induction a
  · rwa [zero_add, zero_add]
  induction b
  · rw [add_zero]
    induction c
    · rw [add_zero]
    · rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)
  · rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
    rw [← coe_add, ← coe_add _ c, coe_le_coe]
    exact add_le_add_left hbc' _

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