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