linarith with abs

Stream: general

[ZHAO Jinxiang]

Is there any tactic like linarith with abs support?

[Mario Carneiro]

you could rewrite with theorems like docs#le_abs and then call linarith

[ZHAO Jinxiang]

For example:

example (a b x: ℝ) (h : a < x ∧ x < b): x + |x - b| = x + (b - x) :=
begin
  refine congr_arg (λ y, x + y) _,
  cases h,
  rw← abs_neg,
  simp,
  exact le_of_lt h_right,
end

Is there any tactic to simplify it?

[Kevin Buzzard]

example (a b x: ℝ) (h : a < x ∧ x < b): x + |x - b| = x + (b - x) :=
begin
  congr',
  rw [abs_sub_comm, abs_eq_self],
  linarith,
end

is a bit shorter