REAL_LE_IMP : thm -> thm

SYNOPSIS
Perform transitivity chaining for non-strict real number inequality.

DESCRIPTION
When applied to a theorem A |- s <= t where s and t have type real, the rule REAL_LE_IMP returns A |- !x1...xn z. t <= z ==> s <= z, where z is some variable and the x1,...,xn are free variables in s and t.

FAILURE CONDITIONS
Fails if applied to a theorem whose conclusion is not of the form `s <= t` for some real number terms s and t.

EXAMPLE
  # REAL_LE_IMP (REAL_ARITH `x:real <= abs(x)`);;
  val it : thm = |- !x z. abs x <= z ==> x <= z

USES
Can make transitivity chaining in goals easier, e.g. by FIRST_ASSUM(MATCH_MP_TAC o REAL_LE_IMP).

SEE ALSO
LE_IMP, REAL_ARITH, REAL_LET_IMP.