proposition: Lemma Rabs_def2_le : forall x a, (Rabs x <= a)%R -> (-a <= x <= a)%R.
proof: Proof. intros x a H. assert (0 <= a)%R. apply Rle_trans with (2 := H). apply Rabs_pos. generalize H. clear H. unfold Rabs. case (Rcase_abs x) ; split. rewrite <- (Ropp_involutive x). apply Ropp_le_contravar. exact H. apply Rlt_le. apply Rlt_le_trans with (1 := r). exact H0. generalize (Rge_le _ _ r). clear r. intro. apply Rle_trans with (2 := H1). rewrite <- Ropp_0. apply Ropp_le_contravar. exact H0. exact H. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)