have : p ≃ 0 := calc
  _ ≃ p             := eqv_refl
  _ ≃ p * 1         := eqv_symm mul_identR
  _ ≃ p * (p * p⁻¹) := mul_substR (eqv_symm mul_inverseR)
  _ ≃ p * (p * 0)   := mul_substR (mul_substR ‹p⁻¹ ≃ 0›)
  _ ≃ p * 0         := mul_substR mul_absorbR
  _ ≃ 0             := mul_absorbR
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
⊢ False
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
this : p ≃ 0
⊢ False