have : n > m := Natural.compare_gt.mp this
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 1
this✝¹ : ord_sgn (compare n m) ≃ 1
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
this : compare n m = Ordering.gt
⊢ Positive (n——m)
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 1
this✝² : ord_sgn (compare n m) ≃ 1
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
this✝ : compare n m = Ordering.gt
this : n > m
⊢ Positive (n——m)