a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ 0 ≤ a
rw [Rat.le_iff_Nonneg]
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
show Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
no goals
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
simp