d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ Nonneg (b - a)
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ Nonneg (c + b - (c + a))
rw [add_sub_add_left_eq_sub]
no goals
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ Nonneg (b - a)
exact ab