proposition: Lemma Rabs_def2b : forall x a : R, (Rabs x <= a)%R -> (-a <= x <= a)%R.
proof: Proof. intros x a H. split. case (Rcase_abs x); intros. rewrite Rabs_left with (1 := r) in H. rewrite <- (Ropp_involutive x). apply Ropp_le_contravar with (1 := H). apply Rle_trans with 0%R. rewrite <- Ropp_0. apply Ropp_le_contravar. apply Rle_trans with (2 := H). apply Rabs_pos. apply Rge_le with (1 := r). apply Rle_trans with (2 := H). apply RRle_abs. Qed.
imports: Gappa_common Gappa_pred_nzr