transitivity (tri n₁) using LT.lt, LE.le
case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri + m₁
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri

case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁.tri ≤ n₁.tri + m₁