proposition: Theorem Rabs_ge_inv : forall x y, (x <= Rabs y)%R -> (y <= -x \/ x <= y)%R.
proof: Proof. intros x y. unfold Rabs. case Rcase_abs ; intros Hy Hxy. left. apply Ropp_le_cancel. now rewrite Ropp_involutive. now right. Qed.
imports: Coq(Psatz Reals ZArith) Zaux