Definition p0n4  : 0 <> 4  := O_S 3.
