transitivity (x₂ - y₁)
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₂
case left
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₁

case right
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₂ - y₁ ≤ x₂ - y₂