fact: Definition positive_apart_zero (z : R) (Pz : 0 < z) : z ≶ 0 := pseudo_order_lt_apart_flip 0 z Pz.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings