proposition: Lemma Rabs_def1_le : forall x a, (x <= a)%R -> (-a <= x)%R -> (Rabs x <= a)%R.
proof: Proof. intros. case (Rcase_abs x) ; intros. rewrite (Rabs_left _ r). rewrite <- (Ropp_involutive a). apply Ropp_le_contravar. exact H0. rewrite (Rabs_right _ r). exact H. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)