∀ {m n : PosNum} (motive : (x : Ordering) → Ordering.casesOn x (↑m < ↑n) (m = n) (↑n < ↑m) → Prop) (x : Ordering)
  (x_1 : Ordering.casesOn x (↑m < ↑n) (m = n) (↑n < ↑m)),
  (∀ (h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)), motive Ordering.lt h) →
    (∀ (h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)), motive Ordering.eq h) →
      (∀ (h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)), motive Ordering.gt h) → motive x x_1