[Agda] ¬ 0# ? 1#

[Sergei Meshveliani]

People,
this is a question about Standard library.
I write

  module _ {α α=} (R : CommutativeRing α α=)
                  (open CommutativeRing R using (0#; 1#; ...))
                  (0≉1 : ¬ 0# ≈ 1#)
  ...


But probably  0≉1  needs to be an axiom in RingWithOne (and in
CommutativeRing). Is such in Standard library?

Thanks,

------
Sergei