proposition: Lemma RmaxAbs : forall (p q:R) r, p <= q -> q <= r -> Rabs q <= Rmax (Rabs p) (Rabs r).
proof: Proof. intros p q r H' H'0; case (Rle_or_lt 0 p); intros H'1. - repeat rewrite Rabs_right; auto with real. + apply Rle_trans with r; auto with real. apply RmaxLess2; auto. + apply Rge_trans with p; auto with real; apply Rge_trans with q; auto with real. + apply Rge_trans with p; auto with real. - rewrite (Rabs_left p); auto. case (Rle_or_lt 0 q); intros H'2. + repeat rewrite Rabs_right; auto with real. * apply Rle_trans with r; auto. apply RmaxLess2; auto. * apply Rge_trans with q; auto with real. + rewrite (Rabs_left q); auto. case (Rle_or_lt 0 r); intros H'3. * repeat rewrite Rabs_right; auto with real. apply Rle_trans with (- p); auto with real. apply RmaxLess1; auto. * rewrite (Rabs_left r); auto. apply Rle_trans with (- p); auto with real. apply RmaxLess1; auto. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp