Definition p0n6  : 0 <> 6  := O_S 5.
