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