proposition: Lemma QposInf_le_QinfLe (x y: QposInf): QposInf_le x y → le x y.
proof: Proof. destruct x, y; auto. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid Coq.Arith.Arith CoRN.model.rings.Qring CoRN.model.structures.QposInf CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra MathClasses.implementations.stdlib_rationals MathClasses.theory.setoids