simp [compare, instOrdNat, compareOfLessAndEq]
m n : Nat
h : m < n
⊢ compare m n = Ordering.lt
m n : Nat
h : m < n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.lt