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

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x