Eliminate abs/max/min before reifying real inequalities with simp iff lemmas

When writing a reflective tactic for polynomial (in)equalities over ℝ, you can support |e|, max and min in comparison atoms without extending the reifier. Run simp only [abs_le, abs_lt, le_abs, lt_abs, max_le_iff, max_lt_iff, le_max_iff, lt_max_iff, le_min_iff, lt_min_iff, min_le_iff, min_lt_iff, ge_iff_le, gt_iff_lt] on the goal first, wrapped in try because simp fails when nothing changes. Each lemma turns the atom into a boolean combination of plain polynomial comparisons, e.g. |a| ≤ b becomes -b ≤ a ∧ a ≤ b. This covers abs on either side of < and ≤, but not |a| = b.