feat: 0 < a → 0 < a + b (leanprover-community#37641)

Author: vihdzp

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -153,6 +153,25 @@ theorem one_lt_of_gt (h : a < b) : 1 < b :=
 alias LT.lt.pos := pos_of_gt
 @[to_additive existing] alias LT.lt.one_lt := one_lt_of_gt
 
+@[to_additive]
+theorem Left.one_lt_mul_of_left [MulLeftMono α] (ha : 1 < a) (b : α) : 1 < a * b :=
+  Left.one_lt_mul_of_lt_of_le ha (one_le b)
+
+@[to_additive]
+theorem Left.one_lt_mul_of_right [MulLeftStrictMono α] (hb : 1 < b) (a : α) : 1 < a * b :=
+  Left.one_lt_mul_of_le_of_lt (one_le a) hb
+
+@[to_additive]
+theorem Right.one_lt_mul_of_left [MulRightStrictMono α] (ha : 1 < a) (b : α) : 1 < a * b :=
+  Right.one_lt_mul_of_lt_of_le ha (one_le b)
+
+@[to_additive]
+theorem Right.one_lt_mul_of_right [MulRightMono α] (hb : 1 < b) (a : α) : 1 < a * b :=
+  Right.one_lt_mul_of_le_of_lt (one_le a) hb
+
+@[to_additive add_pos_of_left] alias one_lt_mul_of_left := Left.one_lt_mul_of_left
+@[to_additive add_pos_of_right] alias one_lt_mul_of_right := Right.one_lt_mul_of_right
+
 end Preorder
 
 section PartialOrder

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -911,16 +911,17 @@ theorem add_succ (o₁ o₂ : Ordinal) : o₁ + succ o₂ = succ (o₁ + o₂) :
 protected theorem one_le_iff_ne_zero {o : Ordinal} : 1 ≤ o ↔ o ≠ 0 :=
   Order.one_le_iff_ne_zero
 
+@[deprecated add_pos_of_right (since := "2026-04-04")]
 theorem succ_pos (o : Ordinal) : 0 < succ o :=
-  bot_lt_succ o
+  add_pos_of_right zero_lt_one o
 
--- TODO: generalize to `SuccAddOrder`
+@[deprecated add_pos_of_right (since := "2026-04-04")]
 theorem add_one_ne_zero (o : Ordinal) : o + 1 ≠ 0 :=
-  (succ_pos o).ne'
+  (add_pos_of_right zero_lt_one o).ne'
 
-@[deprecated add_one_ne_zero (since := "2026-02-27")]
+@[deprecated add_pos_of_right (since := "2026-02-27")]
 theorem succ_ne_zero (o : Ordinal) : succ o ≠ 0 :=
-  add_one_ne_zero o
+  (add_pos_of_right zero_lt_one o).ne'
 
 @[deprecated Order.lt_one_iff (since := "2026-03-24")]
 theorem lt_one_iff_zero {a : Ordinal} : a < 1 ↔ a = 0 :=

Mathlib/SetTheory/Ordinal/Exponential.lean

@@ -57,7 +57,7 @@ theorem opow_zero (a : Ordinal) : a ^ (0 : Ordinal) = 1 := by
 @[simp]
 theorem opow_add_one (a b : Ordinal) : a ^ (b + 1) = a ^ b * a := by
   obtain rfl | h := eq_or_ne a 0
-  · rw [zero_opow (add_one_ne_zero b), mul_zero]
+  · rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]
   · rw [opow_of_ne_zero h, opow_of_ne_zero h]
     exact limitRecOn_succ ..
 
@@ -483,7 +483,7 @@ theorem lt_omega0_opow {a b : Ordinal} (hb : b ≠ 0) :
 
 theorem lt_omega0_opow_succ {a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a < ω ^ b * n := by
   refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩
-  obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (add_one_ne_zero b)).1 ha
+  obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (add_pos_of_right zero_lt_one b).ne').1 ha
   refine ⟨n, hn.trans_le ?_⟩
   grw [lt_succ_iff.1 hc]
   exact omega0_pos

Mathlib/SetTheory/Ordinal/Topology.lean

@@ -79,7 +79,8 @@ theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) :
     have hlub : IsLUB t (sSup t) := isLUB_csSup hne hbdd
     let ⟨y, hyt⟩ := hne
     classical
-      refine ⟨sSup t + 1, add_one_ne_zero _, fun x _ => if x ∈ t then x else y, fun x _ => ?_, ?_⟩
+      refine ⟨_, (add_pos_of_right zero_lt_one (sSup t)).ne',
+        fun x _ ↦ if x ∈ t then x else y, fun x _ => ?_, ?_⟩
       · simp only
         split_ifs with h <;> exact hts ‹_›
       · refine le_antisymm (bsup_le fun x _ => ?_) (csSup_le hne fun x hx => ?_)

Mathlib/SetTheory/Ordinal/Veblen.lean

@@ -117,8 +117,8 @@ theorem veblenWith_mem_range : veblenWith f o a ∈ range f := by
     simp
 
 theorem veblenWith_add_one (o : Ordinal) : veblenWith f (o + 1) = deriv (veblenWith f o) := by
-  rw [deriv_eq_enumOrd (isNormal_veblenWith hf o), veblenWith_of_ne_zero f (add_one_ne_zero _),
-    derivFamily_eq_enumOrd]
+  rw [deriv_eq_enumOrd (isNormal_veblenWith hf o),
+    veblenWith_of_ne_zero f (add_pos_of_right zero_lt_one _).ne', derivFamily_eq_enumOrd]
   · apply congr_arg
     ext a
     rw [mem_iInter]