case mpr =>
  intro (_ : sgn (n——m) ≃ 1)
  show Positive (n——m)
  have : ord_sgn (compare n m) ≃ (1:Difference ℕ) := ‹sgn (n——m) ≃ 1›
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt := this
  have : compare n m = Ordering.gt := ord_sgn_inject this
  have : n > m := Natural.compare_gt.mp this
  have : Positive (n——m) := pos_diff_gt.mpr this
  exact this
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 1 → Positive (n——m)
no goals