have r₂: a + d < b + d := add_lt_add_right h₁ d
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c < b + d
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d < b + d
⊢ a + c < b + d