proposition: Lemma Q2R_max: forall x y : Q, Q2R (Qminmax.Qmax x y) = Rmax (Q2R x) (Q2R y).
proof: Proof. intros x y. destruct (Qlt_le_dec x y) as [Hlt|Hle]. - rewrite Qminmax.Q.max_r, Rmax_right. + reflexivity. + apply Qreals.Qle_Rle, Qlt_le_weak, Hlt. + apply Qlt_le_weak, Hlt. - rewrite Qminmax.Q.max_l, Rmax_left. + reflexivity. + apply Qreals.Qle_Rle, Hle. + apply Hle. Qed.
imports: Reals ZArith QArith Lra Lia