∀[a,b:ℤ].  (a * b ≠ 0) supposing (b ≠ 0 and a ≠ 0)
{ Auto }
1. a : ℤ
2. b : ℤ
3. a ≠ 0
4. b ≠ 0
⊢ a * b ≠ 0