proposition: Lemma QposInfEq_trans x y z : QposInfEq x y -> QposInfEq y z -> QposInfEq x z.
proof: Proof. destruct x as [x|], y as [y|], z as [z|]; simpl; try tauto. apply Qeq_trans. Qed.
imports: Coq.QArith.QArith CoRN.model.totalorder.QposMinMax