proposition: Theorem Rabs_le_inv : forall x y, (Rabs x <= y)%R -> (-y <= x <= y)%R.
proof: Proof. intros x y Hxy. split. apply Rle_trans with (- Rabs x)%R. now apply Ropp_le_contravar. apply Ropp_le_cancel. rewrite Ropp_involutive, <- Rabs_Ropp. apply RRle_abs. apply Rle_trans with (2 := Hxy). apply RRle_abs. Qed.
imports: Coq(Psatz Reals ZArith) Zaux