fact: Definition Qpos_le_total (x y : Qpos) : {proj1_sig x <= proj1_sig y} + {proj1_sig y <= proj1_sig x} := match Qlt_le_dec_fast (proj1_sig x) (proj1_sig y) with | left p => left _ (Qlt_le_weak _ _ p) | right p => right _ p end.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder