anchor.diff:      let max_tm = (parse_term @"max:real->real->real")
       let min_tm = (parse_term @"min:real->real->real")
       let div_conv = REWR_CONV real_div
  +
       let rec REAL_POLY_CONV tm = 
  -        if not(is_comb tm) || is_ratconst tm then REFL tm
  -        else 
  -            let lop, r = Choice.get <| dest_comb tm
  -            if lop = neg_tm then 
  -                let th1 = AP_TERM lop (REAL_POLY_CONV r)
  -                TRANS th1 (REAL_POLY_NEG_CONV(Choice.get <| rand(concl <| Choice.get th1)))
  -            elif lop = inv_tm then 
  -                let th1 = AP_TERM lop (REAL_POLY_CONV r)
  -                TRANS th1 (TRY_CONV REAL_RAT_INV_CONV (Choice.get <| rand(concl <| Choice.get th1)))
  -            elif lop = abs_tm then AP_TERM lop (REAL_POLY_CONV r)
  -            elif not(is_comb lop) then REFL tm
  +        choice {
  +            if not(is_comb tm) || is_ratconst tm then 
  +                return! REFL tm
               else 
  -                let op, l = Choice.get <| dest_comb lop
  -                if op = pow_tm then 
  -                    let th1 = AP_THM (AP_TERM op (REAL_POLY_CONV l)) r
  -                    TRANS th1 (TRY_CONV REAL_POLY_POW_CONV (Choice.get <| rand(concl <| Choice.get th1)))
  -                elif op = add_tm || op = mul_tm || op = sub_tm then 
  -                    let th1 = MK_COMB(AP_TERM op (REAL_POLY_CONV l), REAL_POLY_CONV r)
  -                    let fn = 
  -                        if op = add_tm then REAL_POLY_ADD_CONV
  -                        elif op = mul_tm then REAL_POLY_MUL_CONV
  -                        else REAL_POLY_SUB_CONV
  -                    TRANS th1 (fn(Choice.get <| rand(concl <| Choice.get th1)))
  -                elif op = div_tm then 
  -                    let th1 = div_conv tm
  -                    TRANS th1 (REAL_POLY_CONV(Choice.get <| rand(concl <| Choice.get th1)))
  -                elif op = min_tm || op = max_tm then MK_COMB(AP_TERM op (REAL_POLY_CONV l), REAL_POLY_CONV r)
  -                else REFL tm
  +                let! lop, r = dest_comb tm
  +                if lop = neg_tm then 
  +                    let! th1 = AP_TERM lop (REAL_POLY_CONV r)
  +                    let! tm1 = rand(concl th1)
  +                    return! TRANS (Choice.result th1) (REAL_POLY_NEG_CONV tm1)
  +                elif lop = inv_tm then 
  +                    let! th1 = AP_TERM lop (REAL_POLY_CONV r)
  +                    let! tm1 = rand(concl th1)
  +                    return! TRANS (Choice.result th1) (TRY_CONV REAL_RAT_INV_CONV tm1)
  +                elif lop = abs_tm then 
  +                    return! AP_TERM lop (REAL_POLY_CONV r)
  +                elif not(is_comb lop) then 
  +                    return! REFL tm
  +                else 
  +                    let! op, l = dest_comb lop
  +                    if op = pow_tm then 
  +                        let! th1 = AP_THM (AP_TERM op (REAL_POLY_CONV l)) r
  +                        let! tm1 = rand(concl th1)
  +                        return! TRANS (Choice.result th1) (TRY_CONV REAL_POLY_POW_CONV tm1)
  +                    elif op = add_tm || op = mul_tm || op = sub_tm then 
  +                        let! th1 = MK_COMB(AP_TERM op (REAL_POLY_CONV l), REAL_POLY_CONV r)
  +                        let fn = 
  +                            if op = add_tm then REAL_POLY_ADD_CONV
  +                            elif op = mul_tm then REAL_POLY_MUL_CONV
  +                            else REAL_POLY_SUB_CONV
  +                        let! tm1 = rand(concl th1)
  +                        return! TRANS (Choice.result th1) (fn tm1)
  +                    elif op = div_tm then 
  +                        let! th1 = div_conv tm
  +                        let! tm1 = rand(concl th1)
  +                        return! TRANS (Choice.result th1) (REAL_POLY_CONV tm1)
  +                    elif op = min_tm || op = max_tm then 
  +                        return! MK_COMB(AP_TERM op (REAL_POLY_CONV l), REAL_POLY_CONV r)
  +                    else 
  +                        return! REFL tm
  +        }
  +
       REAL_POLY_CONV
   
   (* ------------------------------------------------------------------------- *)
  
positive.code:     let x2 = (parse_term @"x2:real")
      let y1 = (parse_term @"y1:real")
      let y2 = (parse_term @"y2:real")
      let dest_le = Choice.get << dest_binop(parse_term @"(<=)")
      let dest_div = Choice.get << dest_binop(parse_term @"(/)")
      let RAW_REAL_RAT_LE_CONV tm = 
          let l, r = dest_le tm
          let lx, ly = dest_div l
          let rx, ry = dest_div r
          let th0 = 
              INST [lx, x1
                    ly, y1
                    rx, x2
                    ry, y2] pth
          let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0
          let th2 = (BINOP_CONV REAL_INT_MUL_CONV
                     |> THENC <| REAL_INT_LE_CONV)(Choice.get <| rand(concl <| Choice.get th1))
          TRANS th1 th2
      BINOP_CONV REAL_INT_RAT_CONV
      |> THENC <| RAW_REAL_RAT_LE_CONV
  
  
negative.code: 
    let RAW_REAL_RAT_ADD_CONV tm = 
      choice {
           let! r1, r2 = dest_addop tm
           let! x1', y1' = dest_divop r1
           let! x2', y2' = dest_divop r2
           let! x1n = dest_realintconst x1'
           let! y1n = dest_realintconst y1'
           let! x2n = dest_realintconst x2'
  