apply Nat.mul_pos
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < x * y
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0

case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0