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