Definition p0n64 : 0 <> 64 := O_S 63.
