have (AltPositive.intro (a : ℤ) (b : ℤ) a_pos b_pos x_eqv) :=
  ‹AltPositive x›
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
⊢ Positive x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x