a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
⊢ 0 ≤ a * b
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b
let ⟨n, hn⟩ := eq_ofNat_of_zero_le ha
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ a * b
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
⊢ 0 ≤ a * b
let ⟨m, hm⟩ := eq_ofNat_of_zero_le hb
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ ↑(n * m)
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ a * b
rw [hn, hm, ← ofNat_mul]
no goals
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ ↑(n * m)
apply ofNat_nonneg