case mp =>
  intro (_ : dist p q ≃ 0)
  show p ≃ q
  have : abs (p - q) ≃ 0 := AA.eqv_substL dist_abs ‹dist p q ≃ 0›
  have : p - q ≃ 0 := abs_zero.mp this
  have : p ≃ q := sub_eqv_zero_iff_eqv.mp this
  exact this
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ dist p q ≃ 0 → p ≃ q
no goals