Definition p0n16 : 0 <> 16 := O_S 15.
