proposition: Lemma RmaxRmult : forall (p q:R) r, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q.
proof: Proof. intros p q r H; unfold Rmax. case (Rle_dec p q); case (Rle_dec (r * p) (r * q)); auto; intros H1 H2; auto. - case H; intros E1. + case H1; auto with real. + rewrite <- E1; repeat rewrite Rmult_0_l; auto. - case H; intros E1. + case H2; auto with real. apply Rmult_le_reg_l with (r := r); auto. + rewrite <- E1; repeat rewrite Rmult_0_l; auto. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp