proposition: Lemma Rmax_comm : forall x y:R, Rmax x y = Rmax y x.
proof: Proof. intros p q; unfold Rmax; case (Rle_dec p q); case (Rle_dec q p); auto; intros H1 H2; apply Rle_antisym; auto with real. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp