fact: Definition QposInf_le (x y: QposInf) : Prop := match y with | QposInfinity => True | Qpos2QposInf y' => match x with | QposInfinity => False | Qpos2QposInf x' => proj1_sig x' <= proj1_sig y' end end.
imports: Coq.QArith.QArith CoRN.model.totalorder.QposMinMax