4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederforall aa,ab:s . aa <= ab => p
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maedernot (s(n) <= 0)
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maederi * q <= j * p
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder(i * q) <= (j * p)
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maederc * (a + b) = (c * a) + (c * b)
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder(a + b) * c = (a * c) + (b * c)