case mk'
b c : ℚ
n : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs n) den✝
⊢ Rat.Nonneg (mk' n den✝) ∨ Rat.Nonneg (-mk' n den✝)
a b c : ℚ
⊢ Rat.Nonneg a ∨ Rat.Nonneg (-a)
cases' a with n
no goals
case mk'
b c : ℚ
n : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs n) den✝
⊢ Rat.Nonneg (mk' n den✝) ∨ Rat.Nonneg (-mk' n den✝)
exact Or.imp_right neg_nonneg_of_nonpos (le_total 0 n)