a b c : ℚ
⊢ Rat.Nonneg (a - a)
a b c : ℚ
⊢ a ≤ a
rw [Rat.le_iff_Nonneg]
a b c : ℚ
⊢ Rat.Nonneg (a - a)
a b c : ℚ
⊢ Rat.Nonneg (a - a)
show Rat.Nonneg (a - a)
a b c : ℚ
⊢ Rat.Nonneg 0
a b c : ℚ
⊢ Rat.Nonneg (a - a)
rw [sub_self]
no goals
a b c : ℚ
⊢ Rat.Nonneg 0
exact le_refl (0 : ℤ)