proposition: Lemma QposInf_min_lb_l : forall x y, QposInf_le (QposInf_min x y) x.
proof: Proof. intros [x|] [y|]; simpl; try auto. apply Qpos_min_lb_l. apply Qle_refl. Qed.
imports: Coq.QArith.QArith CoRN.model.totalorder.QposMinMax