case mp =>
  intro (_ : p/q ≃ 1)
  show p ≃ q
  calc
    _ ≃ p             := eqv_refl
    _ ≃ p * 1         := eqv_symm mul_identR
    _ ≃ p * (q⁻¹ * q) := mul_substR (eqv_symm mul_inverseL)
    _ ≃ (p * q⁻¹) * q := eqv_symm mul_assoc
    _ ≃ (p/q) * q     := mul_substL (eqv_symm div_mul_recip)
    _ ≃ 1 * q         := mul_substL ‹p/q ≃ 1›
    _ ≃ q             := mul_identL
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q
no goals