fact: Definition QposInfEq (a b:QposInf) := match a, b with | Qpos2QposInf x, Qpos2QposInf y => Qeq (proj1_sig x) (proj1_sig y) | QposInfinity, QposInfinity => True | _, _ => False end.
imports: Coq.QArith.QArith CoRN.model.totalorder.QposMinMax