split
n m : Nat
x✝ : lt n m
⊢ (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
case isTrue
n m : Nat
x✝ : lt n m
h✝ : n < m
⊢ Ordering.lt = Ordering.lt

case isFalse
n m : Nat
x✝ : lt n m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt