fact: Definition QposInf_min (x y : QposInf) : QposInf := match x with | QposInfinity => y | Qpos2QposInf x' => match y with | QposInfinity => x' | Qpos2QposInf y' => Qpos2QposInf (Qpos_min x' y') end end.
imports: Coq.QArith.QArith CoRN.model.totalorder.QposMinMax