proposition: Lemma Rmax_stable_in_negreal : forall x y:negreal, Rmax x y < 0.
proof: Proof. intros; unfold Rmax; case (Rle_dec x y); intro; [ apply (cond_neg y) | apply (cond_neg x) ]. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp