anchor.diff:                   REWRITE_TAC [real_abs; real_gt; real_ge]
                    |> THEN <| COND_CASES_TAC
                    |> THEN <| ASM_REWRITE_TAC [real_lt])
  +
           let pth_max = 
               prove
                   ((parse_term @"P(max x y) <=> (y >= x /\ P y) \/ (x > y /\ P x)"), 
                    REWRITE_TAC [real_max; real_gt; real_ge]
                    |> THEN <| COND_CASES_TAC
                    |> THEN <| ASM_REWRITE_TAC [real_lt])
  +
           let pth_min = 
               prove
                   ((parse_term @"P(min x y) <=> (y >= x /\ P x) \/ (x > y /\ P y)"), 
                    REWRITE_TAC [real_min; real_gt; real_ge]
                    |> THEN <| COND_CASES_TAC
                    |> THEN <| ASM_REWRITE_TAC [real_lt])
  +
           let abs_tm = (parse_term @"real_abs")
           let p_tm = (parse_term @"P:real->bool")
           let x_tm = (parse_term @"x:real")
  
positive.code:         let is_max = is_binop(parse_term @"real_max")
          let is_min = is_binop(parse_term @"real_min")
  
          let is_abs t = is_comb t && Choice.get <| rator t = abs_tm
  
          let eliminate_construct p c tm = 
              let t = Choice.get <| find_term (fun t -> p t && free_in t tm) tm
              let v = genvar(Choice.get <| type_of t)
              let th0 = SYM(BETA_CONV(Choice.get <| mk_comb(Choice.get <| mk_abs(v, Choice.get <| subst [v, t] tm), t)))
              let p, ax = Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th0))
              CONV_RULE (RAND_CONV(BINOP_CONV(RAND_CONV BETA_CONV))) 
                  (TRANS th0 (c p ax))
  
          let elim_abs = 
              eliminate_construct is_abs (fun p ax -> 
                      INST [p, p_tm
                            Choice.get <| rand ax, x_tm] pth_abs)
  
          let elim_max = 
              eliminate_construct is_max (fun p ax -> 
                      let ax, y = Choice.get <| dest_comb ax
                      INST [p, p_tm
                            Choice.get <| rand ax, x_tm
                            y, y_tm] pth_max)
  
          let elim_min = 
              eliminate_construct is_min (fun p ax -> 
                      let ax, y = Choice.get <| dest_comb ax
                      INST [p, p_tm
                            Choice.get <| rand ax, x_tm
                            y, y_tm] pth_min)
  
          FIRST_CONV [elim_abs; elim_max; elim_min]
      fun (mkconst, EQ, GE, GT, NORM, NEG, ADD, MUL, PROVER) -> 
          GEN_REAL_ARITH_001(mkconst, EQ, GE, GT, NORM, NEG, ADD, MUL, ABSMAXMIN_ELIM_CONV1, ABSMAXMIN_ELIM_CONV2, PROVER)
  
  
negative.code: 
      let contradictory p (e, _) = 
          (is_undefined e && not(p num_0)) 
          // It seems fine to use Option.get here
          || (dom e = [one_tm] && not(p(Option.get <| apply e one_tm)))
  
      let rec linear_ineqs vars (les, lts) = 
  