exact AsRatio.intro a b ‹Integer.Nonzero b› eqv_refl
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
a b : ℤ
x✝ : Integer.Nonzero b
⊢ AsRatio (from_integer a / from_integer b)
no goals