have r₂ : a + d ≤ b + d := add_le_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