apply Iff.intro
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x ↔ AltPositive x
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x