theorem :: NEWTON03:95

for a, b being non trivial Nat
for c being non zero Nat holds (a |-count b) * (b |-count c) <= a |-count c