proposition: Lemma Qmin_nonneg (x y: Q): 0 <= x -> 0 <= y -> 0 <= Qmin x y.
proof: Proof. apply Q.min_glb; assumption. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax