Definition p0n1  : 0 <> 1  := O_S 0.
