have r₂: a + d < b + d := Int.add_lt_add_right h₁ d
a b c d : Int
h₁ : a < b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d
a b c d : Int
h₁ : a < b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d < b + d
⊢ a + c < b + d