sub_le — Mathlib

English

If b ≤ a, then c ≤ a − b is equivalent to b + c ≤ a.

Русский

Если b ≤ a, то c ≤ a − b эквивалентно b + c ≤ a.

LaTeX

$$$\forall a\,\forall b\,\forall c:\; (b \le a) \to (c \le a - b) \iff (b + c \le a).$$$

Lean4

theorem sub_le {a b c : Ordinal} : a - b ≤ c ↔ a ≤ b + c :=
  by
  refine ⟨fun h ↦ (le_add_sub a b).trans (add_le_add_left h _), fun h ↦ ?_⟩
  obtain h' | h' := le_or_gt b a
  · rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']
  · simp [sub_eq_zero_of_lt h']

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