case mp =>
  intro (h : compare n m = Ordering.lt)
  show lt n m
  simp only [compare, Ord.compare, compareOfLessAndEq] at h
  split at h
  case isTrue =>
    have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
    exact this
  case isFalse =>
    split at h <;> contradiction
n m : Nat
⊢ compare n m = Ordering.lt → lt n m
no goals