Definition p0n5  : 0 <> 5  := O_S 4.
