fact: Definition Qpos_min_irred : forall x y: Qpos, {QposEq (Qpos_min x y) x} + {QposEq (Qpos_min x y) y} := @meet_irred Qto.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder