proposition: Theorem Rabs_ge : forall x y, (y <= -x \/ x <= y)%R -> (x <= Rabs y)%R.
proof: Proof. intros x y [Hyx|Hxy]. apply Rle_trans with (-y)%R. apply Ropp_le_cancel. now rewrite Ropp_involutive. rewrite <- Rabs_Ropp. apply RRle_abs. apply Rle_trans with (1 := Hxy). apply RRle_abs. Qed.
imports: Coq(Psatz Reals ZArith) Zaux