I started learning Haskell recently and in my class right now, we have constructed a Peano number class and instanced it in the Num typeclass.
During lecture, my professor claimed that depending on whether you viewed the successor function as S x = x + 1 or S x = 1 + x, the appropriate successor case for the multiplication definition would be different. Respectively:
x * S y = x * y + x
x * S y = x + x * y
Moreover, he claimed that using the first of these two choices is preferable because it is lazier but I'm having trouble seeing how this is the case.
We looked at the example in which the addition definition of
x + S y = S (x + y)
is better than
x + S y = S x + y
because evaluating x + y == z occurs much faster but I can't find an analogous case for multiplication.
The lecture notes are here: http://cmsc-16100.cs.uchicago.edu/2014/Lectures/lecture-02.php
Laziness is not about speed but what is available how soon.
With x * S y = x * y + x then you can answer infinity * 2 > 5 very quickly, because it will expand as so:
infinity * (S (S Z)) > 5
infinity * (S Z) + infinity > 5
infinity * Z + infinity + infinity > 5
infinity + infinity > 5
(from there the rest is trivial)
However, I don't think it is all as good as your professor claimed! Try to expand out 2 * infinity > 5 in this formalism and you'll be disappointed (or busy for a very long time :-P). On the other hand, with the other definition of multiplication, you do get an answer there.
Now, if we have the "good" definition of addition, I think it should be the case that you can get an answer with infinities in either position. And indeed, I checked the source of a few Haskell packages that define Nats, and indeed they prefer x * S y = x + x * y rather than the way your professor claimed was better.