English
For all a,b,c in EReal, under nondegenerate bounds, a ≤ c − b if and only if a + b ≤ c.
Русский
Для всех a,b,c ∈ EReal при отсутствии крайних случаев верно: a ≤ c − b тогда и только тогда, когда a + b ≤ c.
LaTeX
$$$\forall a,b,c \in \mathrm{EReal},\ (b \neq \bot \lor c \neq \top) \land (b \neq \top \lor c \neq \bot) \Rightarrow (a \le c - b \iff a + b \le c)$$$
Lean4
theorem le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) : a ≤ c - b ↔ a + b ≤ c := by
induction b with
| bot =>
simp only [ne_eq, not_true_eq_false, false_or] at hb
simp only [sub_bot hb, le_top, add_bot, bot_le]
| coe b => rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]
| top =>
simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢
refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
by_contra ha
exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)
