d : ℕ
a b : ℤ√↑d
⊢ Nonneg a → Nonneg b → Nonneg (a * b)
d : ℕ
a b : ℤ√↑d
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b
simp_rw [← nonneg_iff_zero_le]
no goals
d : ℕ
a b : ℤ√↑d
⊢ Nonneg a → Nonneg b → Nonneg (a * b)
exact nonneg_mul