fact: Definition Zle_total x y : {x <= y} + {y <= x} := match Z_lt_le_dec x y with | left p => left _ (Zlt_le_weak _ _ p) | right p => right _ p end.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder