proposition: Theorem Rnd_ZR_abs : forall (F : R -> Prop) (rnd: R-> R), Rnd_ZR F rnd -> forall x : R, (Rabs (rnd x) <= Rabs x)%R.
proof: Proof. intros F rnd H x. assert (F 0%R). replace 0%R with (rnd 0%R). eapply H. apply Rle_refl. destruct (H 0%R) as (H1, H2). apply Rle_antisym. apply H1. apply Rle_refl. apply H2. apply Rle_refl. destruct (Rle_or_lt 0 x). rewrite Rabs_pos_eq with (1 := H1). rewrite Rabs_pos_eq. now apply (proj1 (H x)). now apply (proj1 (H x)). apply Rlt_le in H1. rewrite Rabs_left1 with (1 := H1). rewrite Rabs_left1. apply Ropp_le_contravar. now apply (proj2 (H x)). now apply (proj2 (H x)). Qed.
imports: Coq(Reals) Raux Defs