proposition: Lemma Rmax_Rlt : forall x y z, Rmax x y < z <-> x < z /\ y < z.
proof: Proof. intros x y z; split. - unfold Rmax; case (Rle_dec x y). + intros xy yz; split;[apply Rle_lt_trans with y|]; assumption. + intros xz xy; split;[|apply Rlt_trans with x;[apply Rnot_le_gt|]];assumption. - intros [h h']; apply Rmax_lub_lt; assumption. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp