anchor.diff:           |> THEN <| MATCH_MP_TAC lemma
            |> THEN <| MATCH_MP_TAC REAL_LT_INV
            |> THEN <| ASM_REWRITE_TAC [])
  +#else
  +    Sequent([],parse_term @"&0 < y1 /\ &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)")
  +#endif
   
   let RAT_LEMMA5 = 
       prove
  
positive.code:                    GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] |>THEN<|
         ONCE_REWRITE_TAC[GSYM REAL_SUB_0] |>THEN<|
         REWRITE_TAC[GSYM REAL_ENTIRE] |>THEN<| REAL_ARITH_TAC)
     let REAL_RABINOWITSCH = 
        prove ((parse_term @"!x y:real. ~(x = y) <=> ?z. (x - y) * z = &1"),
          REPEAT GEN_TAC |>THEN<|
  
negative.code:                                  GSYM REAL_MUL_LNEG])
  
  let RAT_LEMMA4 = 
  #if BUGGY
      prove
          ((parse_term @"&0 < y1 /\ &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)"), 
           let lemma = 
  