proposition: Lemma Rmin_Rmax_overflow: forall x y z M, Rabs x <= M -> Rabs y <= M -> Rmin x y <= z <= Rmax x y -> Rabs z <= M.
proof: Proof. intros x y z M Hx Hy H. case (Rle_or_lt 0 z); intros Hz. rewrite Rabs_right. apply Rle_trans with (1:=proj2 H). generalize (proj2 H). apply Rmax_case_strong. intros; apply Rle_trans with (2:=Hx). apply RRle_abs. intros; apply Rle_trans with (2:=Hy). apply RRle_abs. now apply Rle_ge. rewrite Rabs_left; try assumption. apply Rle_trans with (Rmax (-x) (-y)). rewrite Rmax_opp. apply Ropp_le_contravar, H. apply Rmax_case_strong. intros; apply Rle_trans with (2:=Hx). rewrite <- Rabs_Ropp. apply RRle_abs. intros; apply Rle_trans with (2:=Hy). rewrite <- Rabs_Ropp. apply RRle_abs. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)