proposition: Lemma Qmax_nonneg (x y: Q): 0 <= x -> 0 <= y -> 0 <= Qmax x y.
proof: Proof. intros. apply Qle_trans with x. assumption. apply Q.le_max_l. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax