Definition p0n8  : 0 <> 8  := O_S 7.
