Change list.prod from foldl to foldr

[spl]

@kckennylau says: Was there any point in time where list.prod [t] was definitionally equivalent to t * 1? and was there any point in time where list.prod (x :: L) = x * list.prod L was rfl?

@johoelzl says: I traced it back, it was always foldl. I ported the definition from Lean2's library. I think we should change it to foldr then we get the expected equalities.

[johoelzl]

I remember now why we use foldl: a * b * c = (a * b) * c and [a, b, c].foldl (*) 1 = (((1 * a) * b) * c while [a, b, c].foldr (*) 1 = a * (b * (c * 1)), so the product is associated in the wrong direction.

But I think the definitional equalities are more important.