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