proposition: Lemma Rmin_comm : forall x y:R, Rmin x y = Rmin y x.
proof: Proof. intros; unfold Rmin; case (Rle_dec x y); case (Rle_dec y x); intros; try reflexivity || (apply Rle_antisym; assumption || auto with real). Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp