proposition: Lemma Rmax_case_strong : forall r1 r2 (P:R -> Type), (r2 <= r1 -> P r1) -> (r1 <= r2 -> P r2) -> P (Rmax r1 r2).
proof: Proof. intros r1 r2 P H1 H2; unfold Rmax; case (Rle_dec r1 r2); auto with real. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp