HOL html

Files Index

Theorems Index

R (theorems)

RACONV
RACONV_REFL
RACONV_TYPE
RADICALS_EMPTY_RATIONAL
RADICALS_SUBSET
RADICALS_WELLFORMED
RADICAL_CANONICAL
RADICAL_CANONICAL_TRIVIAL
RADICAL_CIRCLE_CIRCLE_INTERSECTION
RADICAL_EXPRESSION
RADICAL_LINEAR_EQUATION
RADICAL_LINE_CIRCLE_INTERSECTION
RADICAL_LINE_LINE_INTERSECTION
RADICAL_QUADRATIC_EQUATION
RADICAL_RULES
RADICAL_SIMULTANEOUS_LINEAR_EQUATION
RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC
RADICAL_SIMULTANEOUS_QUADRATIC_QUADRATIC
RADICAL_TOP
RADON
RADON_EX_LEMMA
RADON_PARTITION
RADON_S_LEMMA
RADON_V_LEMMA
RAINY_DAY
RAMSEY
RAMSEY_LEMMA1
RAMSEY_LEMMA2
RAMSEY_LEMMA3
RANK_0
RANK_BOUND
RANK_DIM_IM
RANK_EQ_0
RANK_GRAM
RANK_I
RANK_MUL_LE_LEFT
RANK_MUL_LE_RIGHT
RANK_NULLSPACE
RANK_ROW
RANK_SYLVESTER
RANK_TRANSP
RANK_TRIANGLE
RATIONAL_ABS
RATIONAL_ADD
RATIONAL_ALT
RATIONAL_APPROXIMATION
RATIONAL_APPROXIMATION_STRADDLE
RATIONAL_BETWEEN
RATIONAL_CLOSED
RATIONAL_DIV
RATIONAL_INTEGER
RATIONAL_INV
RATIONAL_INV_EQ
RATIONAL_LOWEST
RATIONAL_LOWEST_LEMMA
RATIONAL_MUL
RATIONAL_NEG
RATIONAL_NEG_EQ
RATIONAL_NUM
RATIONAL_POW
RATIONAL_ROOT_INTEGER
RATIONAL_SUB
RAT_LEMMA1
RAT_LEMMA1_SUB
RAT_LEMMA2
RAT_LEMMA3
RAT_LEMMA4
RAT_LEMMA5
RAY
RAY_TO_FRONTIER
RAY_TO_RELATIVE_FRONTIER
RCONE_GE_GT
RCONE_GT_GE
RCONE_GT_NEG
RC_CLOSED
RC_CR
RC_EXPLICIT
RC_IDEMP
RC_INC
RC_INV
RC_MONO
RC_REFL
RC_SC
RC_SYM
RC_TC
RC_TRANS
RE
REACHABLE_INVARIANT
REAL
REALCALC_ABS
REALCALC_ADD
REALCALC_DOWNGRADE
REALCALC_EQ
REALCALC_GE
REALCALC_GT
REALCALC_INT
REALCALC_INV
REALCALC_INV_LEMMA
REALCALC_LE
REALCALC_LT
REALCALC_MUL
REALCALC_NEG
REALCALC_SQRT
REALLIM
REALLIM_1_OVER_LOG
REALLIM_1_OVER_N
REALLIM_ABS
REALLIM_ADD
REALLIM_AT
REALLIM_ATREAL
REALLIM_ATREAL_AT
REALLIM_ATREAL_ID
REALLIM_ATREAL_WITHINREAL
REALLIM_AT_INFINITY
REALLIM_AT_NEGINFINITY
REALLIM_AT_POSINFINITY
REALLIM_COMPLEX
REALLIM_CONG_AT
REALLIM_CONG_ATREAL
REALLIM_CONG_WITHIN
REALLIM_CONG_WITHINREAL
REALLIM_CONST
REALLIM_CONST_EQ
REALLIM_CONTINUOUS_FUNCTION
REALLIM_DIV
REALLIM_EVENTUALLY
REALLIM_IM
REALLIM_INV
REALLIM_LBOUND
REALLIM_LE
REALLIM_LMUL
REALLIM_LMUL_EQ
REALLIM_LOG1_OVER_LOG
REALLIM_LOG_OVER_LOG1
REALLIM_LOG_OVER_N
REALLIM_MAX
REALLIM_MIN
REALLIM_MUL
REALLIM_NA_OVER_N
REALLIM_NEG
REALLIM_NEG_EQ
REALLIM_NULL
REALLIM_NULL_ABS
REALLIM_NULL_ADD
REALLIM_NULL_COMPARISON
REALLIM_NULL_LMUL
REALLIM_NULL_LMUL_EQ
REALLIM_NULL_POW
REALLIM_NULL_POW_EQ
REALLIM_NULL_RMUL
REALLIM_NULL_RMUL_EQ
REALLIM_N_OVER_NA
REALLIM_POSINFINITY_SEQUENTIALLY
REALLIM_POW
REALLIM_POWN
REALLIM_RE
REALLIM_REAL_CONTINUOUS_FUNCTION
REALLIM_RMUL
REALLIM_RMUL_EQ
REALLIM_RPOW
REALLIM_SEQUENTIALLY
REALLIM_SUB
REALLIM_SUM
REALLIM_TRANSFORM
REALLIM_TRANSFORM_BOUND
REALLIM_TRANSFORM_EQ
REALLIM_TRANSFORM_EVENTUALLY
REALLIM_TRANSFORM_STRADDLE
REALLIM_TRANSFORM_WITHINREAL_SET
REALLIM_TRANSFORM_WITHIN_SET
REALLIM_UBOUND
REALLIM_UNIQUE
REALLIM_WITHIN
REALLIM_WITHINREAL
REALLIM_WITHINREAL_ID
REALLIM_WITHINREAL_LE
REALLIM_WITHINREAL_SUBSET
REALLIM_WITHINREAL_WITHIN
REALLIM_WITHIN_LE
REALLIM_WITHIN_OPEN
REALLIM_WITHIN_REAL_OPEN
REALLIM_WITHIN_SUBSET
REALLIM_ZERO_NEGINFINITY
REALLIM_ZERO_POSINFINITY
REAL_ABEL_LEMMA
REAL_ABEL_LIMIT_THEOREM
REAL_ABS_0
REAL_ABS_1
REAL_ABS_ABS
REAL_ABS_BETWEEN
REAL_ABS_BETWEEN1
REAL_ABS_BETWEEN2
REAL_ABS_BOUND
REAL_ABS_BOUNDS
REAL_ABS_CASES
REAL_ABS_CIRCLE
REAL_ABS_DIV
REAL_ABS_EXP
REAL_ABS_INFNORM
REAL_ABS_INF_LE
REAL_ABS_INTEGER_LEMMA
REAL_ABS_INV
REAL_ABS_LE
REAL_ABS_LEMMA
REAL_ABS_LEMMA1
REAL_ABS_MOBIUS
REAL_ABS_MUL
REAL_ABS_NEG
REAL_ABS_NORM
REAL_ABS_NUM
REAL_ABS_NZ
REAL_ABS_PI
REAL_ABS_POS
REAL_ABS_POW
REAL_ABS_REFL
REAL_ABS_RPOW
REAL_ABS_SGN
REAL_ABS_SIGN
REAL_ABS_SIGN2
REAL_ABS_STILLNZ
REAL_ABS_SUB
REAL_ABS_SUB_ABS
REAL_ABS_SUB_INFNORM
REAL_ABS_SUB_NORM
REAL_ABS_SUP_LE
REAL_ABS_TRIANGLE
REAL_ABS_TRIANGLE_LE
REAL_ABS_TRIANGLE_LEMMA
REAL_ABS_TRIANGLE_LT
REAL_ABS_ZERO
REAL_ACS
REAL_ADD
REAL_ADD2_SUB2
REAL_ADD_AC
REAL_ADD_ARG
REAL_ADD_COS
REAL_ADD_LE_SUBST_LHS
REAL_ADD_LE_SUBST_RHS
REAL_ADD_LID_UNIQ
REAL_ADD_RDISTRIB
REAL_ADD_RID
REAL_ADD_RID_UNIQ
REAL_ADD_RINV
REAL_ADD_SIN
REAL_ADD_SUB
REAL_ADD_SUB2
REAL_ADD_TAN
REAL_AFFINITY_EQ
REAL_AFFINITY_LE
REAL_AFFINITY_LT
REAL_ANTIDERIVATIVE_CONTINUOUS
REAL_ANTIDERIVATIVE_INTEGRAL_CONTINUOUS
REAL_ARCH
REAL_ARCH_INV
REAL_ARCH_LEAST
REAL_ARCH_LT
REAL_ARCH_POW
REAL_ARCH_POW2
REAL_ARCH_POW_INV
REAL_ARCH_RDIV_EQ_0
REAL_ARCH_SIMPLE
REAL_ARCH_SIMPLE_LT
REAL_ASN
REAL_ATN_POWSER
REAL_ATN_POWSER_ALT
REAL_ATN_POWSER_DIFFL
REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE
REAL_ATN_POWSER_DIFFS_SUM
REAL_ATN_POWSER_DIFFS_SUMMABLE
REAL_ATN_POWSER_SUMMABLE
REAL_BEPPO_LEVI_DECREASING
REAL_BEPPO_LEVI_INCREASING
REAL_BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING
REAL_BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING
REAL_BINOMIAL_THEOREM
REAL_BOUNDED
REAL_BOUNDED_POS
REAL_BOUNDED_POS_LT
REAL_BOUNDED_REAL_INTERVAL
REAL_BOUNDED_SUBSET
REAL_BOUNDED_UNION
REAL_BOUNDS_LE
REAL_BOUNDS_LT
REAL_CARD_INTSEG_INT
REAL_CLOSED
REAL_CLOSED_DIFF
REAL_CLOSED_EMPTY
REAL_CLOSED_HALFSPACE_GE
REAL_CLOSED_HALFSPACE_LE
REAL_CLOSED_IN
REAL_CLOSED_INTER
REAL_CLOSED_INTERS
REAL_CLOSED_OPEN_INTERVAL
REAL_CLOSED_REAL_INTERVAL
REAL_CLOSED_UNION
REAL_CLOSED_UNIONS
REAL_CLOSED_UNIV
REAL_CNJ
REAL_COMPACT_ATTAINS_INF
REAL_COMPACT_ATTAINS_SUP
REAL_COMPACT_CONTINUOUS_IMAGE
REAL_COMPACT_EQ_BOUNDED_CLOSED
REAL_COMPACT_IMP_BOUNDED
REAL_COMPACT_IMP_CLOSED
REAL_COMPACT_INTERVAL
REAL_COMPACT_UNIFORMLY_CONTINUOUS
REAL_COMPACT_UNION
REAL_COMPLETE
REAL_COMPLETE_SOMEPOS
REAL_COMPLEX_CONTINUOUS_ATREAL
REAL_COMPLEX_CONTINUOUS_WITHINREAL
REAL_COMPLEX_MEASURABLE_ON
REAL_CONTINUOUS_ABS
REAL_CONTINUOUS_ADD
REAL_CONTINUOUS_ADDITIVE_EXTEND
REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR
REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR_INTERVAL
REAL_CONTINUOUS_AT
REAL_CONTINUOUS_ATREAL
REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE
REAL_CONTINUOUS_ATREAL_COMPOSE
REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE
REAL_CONTINUOUS_ATREAL_SQRT_COMPOSE
REAL_CONTINUOUS_ATREAL_WITHINREAL
REAL_CONTINUOUS_ATTAINS_INF
REAL_CONTINUOUS_ATTAINS_SUP
REAL_CONTINUOUS_AT_ACS
REAL_CONTINUOUS_AT_ARG
REAL_CONTINUOUS_AT_ASN
REAL_CONTINUOUS_AT_ATN
REAL_CONTINUOUS_AT_AZIM
REAL_CONTINUOUS_AT_AZIM_COMPOSE
REAL_CONTINUOUS_AT_AZIM_SHARP
REAL_CONTINUOUS_AT_COMPONENT
REAL_CONTINUOUS_AT_COMPOSE
REAL_CONTINUOUS_AT_COS
REAL_CONTINUOUS_AT_DIHV
REAL_CONTINUOUS_AT_DIHV_COMPOSE
REAL_CONTINUOUS_AT_EXP
REAL_CONTINUOUS_AT_ID
REAL_CONTINUOUS_AT_LINEAR_IMAGE
REAL_CONTINUOUS_AT_LOG
REAL_CONTINUOUS_AT_RPOW
REAL_CONTINUOUS_AT_SIN
REAL_CONTINUOUS_AT_SQRT
REAL_CONTINUOUS_AT_SQRT_COMPOSE
REAL_CONTINUOUS_AT_TAN
REAL_CONTINUOUS_AT_TRANSLATION
REAL_CONTINUOUS_AT_VECTOR_ANGLE
REAL_CONTINUOUS_AT_WITHIN
REAL_CONTINUOUS_COMPLEX_COMPONENTS_AT
REAL_CONTINUOUS_COMPLEX_COMPONENTS_WITHIN
REAL_CONTINUOUS_CONST
REAL_CONTINUOUS_CONTINUOUS
REAL_CONTINUOUS_CONTINUOUS1
REAL_CONTINUOUS_CONTINUOUS_ATREAL
REAL_CONTINUOUS_CONTINUOUS_ATREAL_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_AT_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_CONTINUOUS_WITHINREAL_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_WITHIN_COMPOSE
REAL_CONTINUOUS_DIST_AT
REAL_CONTINUOUS_DIST_WITHIN
REAL_CONTINUOUS_DIV
REAL_CONTINUOUS_DIV_AT
REAL_CONTINUOUS_DIV_ATREAL
REAL_CONTINUOUS_DIV_WITHIN
REAL_CONTINUOUS_DIV_WITHINREAL
REAL_CONTINUOUS_FLOOR
REAL_CONTINUOUS_FRAC
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET
REAL_CONTINUOUS_IMP_SQUARE_INTEGRABLE
REAL_CONTINUOUS_INJECTIVE_IFF_MONOTONIC
REAL_CONTINUOUS_INV
REAL_CONTINUOUS_INV_AT
REAL_CONTINUOUS_INV_ATREAL
REAL_CONTINUOUS_INV_WITHIN
REAL_CONTINUOUS_INV_WITHINREAL
REAL_CONTINUOUS_LMUL
REAL_CONTINUOUS_MAX
REAL_CONTINUOUS_MEASURE_IN_HALFSPACE_LE
REAL_CONTINUOUS_MIN
REAL_CONTINUOUS_MUL
REAL_CONTINUOUS_NEG
REAL_CONTINUOUS_NORM_AT
REAL_CONTINUOUS_NORM_WITHIN
REAL_CONTINUOUS_ON
REAL_CONTINUOUS_ON_ACS
REAL_CONTINUOUS_ON_ADD
REAL_CONTINUOUS_ON_ASN
REAL_CONTINUOUS_ON_ATN
REAL_CONTINUOUS_ON_CASES
REAL_CONTINUOUS_ON_CASES_OPEN
REAL_CONTINUOUS_ON_COMPOSE
REAL_CONTINUOUS_ON_COMPOSE_FRAC
REAL_CONTINUOUS_ON_CONST
REAL_CONTINUOUS_ON_CONST_DYADIC_RATIONALS
REAL_CONTINUOUS_ON_COS
REAL_CONTINUOUS_ON_EQ
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN
REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT
REAL_CONTINUOUS_ON_EXP
REAL_CONTINUOUS_ON_ID
REAL_CONTINUOUS_ON_INVERSE
REAL_CONTINUOUS_ON_INVERSE_ALT
REAL_CONTINUOUS_ON_LMUL
REAL_CONTINUOUS_ON_LOG
REAL_CONTINUOUS_ON_MUL
REAL_CONTINUOUS_ON_NEG
REAL_CONTINUOUS_ON_POW
REAL_CONTINUOUS_ON_RMUL
REAL_CONTINUOUS_ON_RPOW
REAL_CONTINUOUS_ON_SIN
REAL_CONTINUOUS_ON_SQRT
REAL_CONTINUOUS_ON_SUB
REAL_CONTINUOUS_ON_SUBSET
REAL_CONTINUOUS_ON_SUM
REAL_CONTINUOUS_ON_TAN
REAL_CONTINUOUS_ON_UNION
REAL_CONTINUOUS_ON_UNION_OPEN
REAL_CONTINUOUS_POW
REAL_CONTINUOUS_REAL_CONTINUOUS_ATREAL
REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_REAL_POLYMONIAL_FUNCTION
REAL_CONTINUOUS_RMUL
REAL_CONTINUOUS_SUB
REAL_CONTINUOUS_TRIVIAL_LIMIT
REAL_CONTINUOUS_WITHIN
REAL_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_WITHINREAL_AZIM_COMPOSE
REAL_CONTINUOUS_WITHINREAL_COMPOSE
REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE
REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE
REAL_CONTINUOUS_WITHINREAL_SUBSET
REAL_CONTINUOUS_WITHIN_ACS
REAL_CONTINUOUS_WITHIN_ACS_STRONG
REAL_CONTINUOUS_WITHIN_ASN
REAL_CONTINUOUS_WITHIN_ASN_STRONG
REAL_CONTINUOUS_WITHIN_ATN
REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE
REAL_CONTINUOUS_WITHIN_COMPOSE
REAL_CONTINUOUS_WITHIN_COS
REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE
REAL_CONTINUOUS_WITHIN_EXP
REAL_CONTINUOUS_WITHIN_ID
REAL_CONTINUOUS_WITHIN_LOG
REAL_CONTINUOUS_WITHIN_RPOW
REAL_CONTINUOUS_WITHIN_SIN
REAL_CONTINUOUS_WITHIN_SQRT
REAL_CONTINUOUS_WITHIN_SQRT_COMPOSE
REAL_CONTINUOUS_WITHIN_SQRT_STRONG
REAL_CONTINUOUS_WITHIN_SUBSET
REAL_CONTINUOUS_WITHIN_TAN
REAL_CONTINUOUS_WITHIN_VECTOR_ANGLE
REAL_CONVERGENT_IMP_BOUNDED
REAL_CONVEX_ADD
REAL_CONVEX_BOUND2_LT
REAL_CONVEX_BOUND_LE
REAL_CONVEX_BOUND_LT
REAL_CONVEX_DISTANCE
REAL_CONVEX_LMUL
REAL_CONVEX_LOCAL_GLOBAL_MINIMUM
REAL_CONVEX_LOWER
REAL_CONVEX_ON
REAL_CONVEX_ON_ASYM
REAL_CONVEX_ON_CONTINUOUS
REAL_CONVEX_ON_DERIVATIVES
REAL_CONVEX_ON_DERIVATIVES_IMP
REAL_CONVEX_ON_DERIVATIVE_INCREASING
REAL_CONVEX_ON_DERIVATIVE_INCREASING_IMP
REAL_CONVEX_ON_DERIVATIVE_SECANT
REAL_CONVEX_ON_DERIVATIVE_SECANT_IMP
REAL_CONVEX_ON_EXP
REAL_CONVEX_ON_JENSEN
REAL_CONVEX_ON_LEFT_SECANT
REAL_CONVEX_ON_LEFT_SECANT_MUL
REAL_CONVEX_ON_RIGHT_SEQUENT
REAL_CONVEX_ON_RIGHT_SEQUENT_MUL
REAL_CONVEX_ON_RPOW
REAL_CONVEX_ON_SECANT_DERIVATIVE
REAL_CONVEX_ON_SECANT_DERIVATIVE_IMP
REAL_CONVEX_ON_SECOND_DERIVATIVE
REAL_CONVEX_ON_SUBSET
REAL_CONVEX_RMUL
REAL_COS
REAL_CX
REAL_DENSE
REAL_DERIVATIVE_IVT_DECREASING
REAL_DERIVATIVE_IVT_INCREASING
REAL_DERIVATIVE_NEG_LEFT_MAXIMUM
REAL_DERIVATIVE_NEG_RIGHT_MINIMUM
REAL_DERIVATIVE_POS_LEFT_MINIMUM
REAL_DERIVATIVE_POS_RIGHT_MAXIMUM
REAL_DERIVATIVE_UNIQUE_ATREAL
REAL_DERIVATIVE_ZERO_MAXMIN
REAL_DIFFERENTIABLE_ADD
REAL_DIFFERENTIABLE_AT
REAL_DIFFERENTIABLE_ATREAL_WITHIN
REAL_DIFFERENTIABLE_AT_ACS
REAL_DIFFERENTIABLE_AT_ASN
REAL_DIFFERENTIABLE_AT_ATN
REAL_DIFFERENTIABLE_AT_COS
REAL_DIFFERENTIABLE_AT_EXP
REAL_DIFFERENTIABLE_AT_LOG
REAL_DIFFERENTIABLE_AT_RPOW
REAL_DIFFERENTIABLE_AT_SIN
REAL_DIFFERENTIABLE_AT_SQRT
REAL_DIFFERENTIABLE_AT_TAN
REAL_DIFFERENTIABLE_BOUND
REAL_DIFFERENTIABLE_CARATHEODORY_ATREAL
REAL_DIFFERENTIABLE_CARATHEODORY_WITHINREAL
REAL_DIFFERENTIABLE_COMPOSE_ATREAL
REAL_DIFFERENTIABLE_COMPOSE_WITHIN
REAL_DIFFERENTIABLE_CONST
REAL_DIFFERENTIABLE_DIV_ATREAL
REAL_DIFFERENTIABLE_DIV_WITHIN
REAL_DIFFERENTIABLE_EQ
REAL_DIFFERENTIABLE_ID
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_WITHINREAL
REAL_DIFFERENTIABLE_INV_ATREAL
REAL_DIFFERENTIABLE_INV_WITHIN
REAL_DIFFERENTIABLE_MUL_ATREAL
REAL_DIFFERENTIABLE_MUL_WITHIN
REAL_DIFFERENTIABLE_NEG
REAL_DIFFERENTIABLE_ON_ADD
REAL_DIFFERENTIABLE_ON_COMPOSE
REAL_DIFFERENTIABLE_ON_CONST
REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE
REAL_DIFFERENTIABLE_ON_DIV
REAL_DIFFERENTIABLE_ON_ID
REAL_DIFFERENTIABLE_ON_IMP_DIFFERENTIABLE_ATREAL
REAL_DIFFERENTIABLE_ON_IMP_DIFFERENTIABLE_WITHIN
REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON
REAL_DIFFERENTIABLE_ON_INV
REAL_DIFFERENTIABLE_ON_MUL
REAL_DIFFERENTIABLE_ON_NEG
REAL_DIFFERENTIABLE_ON_POW
REAL_DIFFERENTIABLE_ON_REAL_OPEN
REAL_DIFFERENTIABLE_ON_SUB
REAL_DIFFERENTIABLE_ON_SUBSET
REAL_DIFFERENTIABLE_ON_SUM
REAL_DIFFERENTIABLE_POW_ATREAL
REAL_DIFFERENTIABLE_POW_WITHIN
REAL_DIFFERENTIABLE_SUB
REAL_DIFFERENTIABLE_TRANSFORM
REAL_DIFFERENTIABLE_TRANSFORM_ATREAL
REAL_DIFFERENTIABLE_TRANSFORM_WITHIN
REAL_DIFFERENTIABLE_WITHIN
REAL_DIFFERENTIABLE_WITHIN_ACS
REAL_DIFFERENTIABLE_WITHIN_ASN
REAL_DIFFERENTIABLE_WITHIN_ATN
REAL_DIFFERENTIABLE_WITHIN_COS
REAL_DIFFERENTIABLE_WITHIN_EXP
REAL_DIFFERENTIABLE_WITHIN_LOG
REAL_DIFFERENTIABLE_WITHIN_SIN
REAL_DIFFERENTIABLE_WITHIN_SQRT
REAL_DIFFERENTIABLE_WITHIN_SUBSET
REAL_DIFFERENTIABLE_WITHIN_TAN
REAL_DIFFSQ
REAL_DIFF_CHAIN_ATREAL
REAL_DIFF_CHAIN_WITHIN
REAL_DINI
REAL_DIV
REAL_DIV_1
REAL_DIV_ADD_DISTRIB
REAL_DIV_DENOM_LE
REAL_DIV_DENOM_LT
REAL_DIV_DISTRIB_2
REAL_DIV_DISTRIB_L
REAL_DIV_DISTRIB_R
REAL_DIV_EQ_0
REAL_DIV_INV
REAL_DIV_LMUL
REAL_DIV_LZERO
REAL_DIV_MUL2
REAL_DIV_POW2
REAL_DIV_POW2_ALT
REAL_DIV_REFL
REAL_DIV_RMUL
REAL_DIV_SQRT
REAL_DOMINATED_CONVERGENCE
REAL_DOUBLE
REAL_DOWN
REAL_DOWN2
REAL_ENTIRE
REAL_EQ_ADD_LCANCEL
REAL_EQ_ADD_LCANCEL_0
REAL_EQ_ADD_RCANCEL
REAL_EQ_ADD_RCANCEL_0
REAL_EQ_AFFINITY
REAL_EQ_IMP_LE
REAL_EQ_INTEGERS
REAL_EQ_INTEGERS_IMP
REAL_EQ_INV
REAL_EQ_INV2
REAL_EQ_LADD
REAL_EQ_LCANCEL_IMP
REAL_EQ_LDIV_EQ
REAL_EQ_LMUL
REAL_EQ_LMUL2
REAL_EQ_LMUL_IMP
REAL_EQ_MUL_LCANCEL
REAL_EQ_MUL_RCANCEL
REAL_EQ_NEG
REAL_EQ_NEG2
REAL_EQ_RADD
REAL_EQ_RCANCEL_IMP
REAL_EQ_RCANCEL_IMP'
REAL_EQ_RDIV_EQ
REAL_EQ_RMUL_IMP
REAL_EQ_SQUARE_ABS
REAL_EQ_SUB_LADD
REAL_EQ_SUB_RADD
REAL_EXISTS
REAL_EXP
REAL_EXP_0
REAL_EXP_13
REAL_EXP_15
REAL_EXP_1_LE_4
REAL_EXP_ADD
REAL_EXP_ADD_MUL
REAL_EXP_BOUND_LEMMA
REAL_EXP_CONVERGES
REAL_EXP_EQ_1
REAL_EXP_FDIFF
REAL_EXP_INJ
REAL_EXP_LE_X
REAL_EXP_LN
REAL_EXP_LOG
REAL_EXP_LT_1
REAL_EXP_MONO_IMP
REAL_EXP_MONO_LE
REAL_EXP_MONO_LT
REAL_EXP_N
REAL_EXP_NEG
REAL_EXP_NEG_MUL
REAL_EXP_NEG_MUL2
REAL_EXP_NZ
REAL_EXP_POS_LE
REAL_EXP_POS_LT
REAL_EXP_SUB
REAL_EXP_SUM
REAL_FACT_NZ
REAL_FLOOR_ADD
REAL_FLOOR_EQ
REAL_FLOOR_LE
REAL_FLOOR_LT
REAL_FLOOR_REFL
REAL_FRAC_ADD
REAL_FRAC_EQ
REAL_FRAC_EQ_0
REAL_FRAC_POS_LT
REAL_FRAC_ZERO
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG
REAL_GT_EXISTS
REAL_GT_IMP_NZ
REAL_HALF
REAL_HALF_DOUBLE
REAL_HREAL_LEMMA1
REAL_HREAL_LEMMA2
REAL_IMP_CNJ
REAL_INDEFINITE_INTEGRAL_CONTINUOUS_LEFT
REAL_INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT
REAL_INFSUM
REAL_INFSUM_0
REAL_INFSUM_ADD
REAL_INFSUM_COMPLEX
REAL_INFSUM_EQ
REAL_INFSUM_LMUL
REAL_INFSUM_NEG
REAL_INFSUM_RESTRICT
REAL_INFSUM_RMUL
REAL_INFSUM_SUB
REAL_INFSUM_UNIQUE
REAL_INF_ASCLOSE
REAL_INF_BOUNDS
REAL_INF_LE_FINITE
REAL_INF_LT_FINITE
REAL_INF_UNIQUE
REAL_INJ
REAL_INTEGER_CLOSURES
REAL_INTEGER_EQ_0
REAL_INTEGRABLE_0
REAL_INTEGRABLE_ADD
REAL_INTEGRABLE_AFFINITY
REAL_INTEGRABLE_COMBINE
REAL_INTEGRABLE_CONST
REAL_INTEGRABLE_CONTINUOUS
REAL_INTEGRABLE_COS_CX
REAL_INTEGRABLE_DECREASING
REAL_INTEGRABLE_DECREASING_PRODUCT
REAL_INTEGRABLE_DECREASING_PRODUCT_UNIV
REAL_INTEGRABLE_DIRICHLET_KERNEL_MUL_EXPAND
REAL_INTEGRABLE_EQ
REAL_INTEGRABLE_INCREASING
REAL_INTEGRABLE_INCREASING_PRODUCT
REAL_INTEGRABLE_INCREASING_PRODUCT_UNIV
REAL_INTEGRABLE_INTEGRAL
REAL_INTEGRABLE_LINEAR
REAL_INTEGRABLE_LMUL
REAL_INTEGRABLE_NEG
REAL_INTEGRABLE_ON
REAL_INTEGRABLE_ON_EMPTY
REAL_INTEGRABLE_ON_LITTLE_SUBINTERVALS
REAL_INTEGRABLE_ON_NULL
REAL_INTEGRABLE_ON_OPEN_INTERVAL
REAL_INTEGRABLE_ON_REFL
REAL_INTEGRABLE_ON_SUBINTERVAL
REAL_INTEGRABLE_ON_SUPERSET
REAL_INTEGRABLE_PERIODIC_OFFSET
REAL_INTEGRABLE_REFLECT
REAL_INTEGRABLE_REFLECT_AND_ADD
REAL_INTEGRABLE_RESTRICT_INTER
REAL_INTEGRABLE_RESTRICT_UNIV
REAL_INTEGRABLE_RMUL
REAL_INTEGRABLE_SIN_AND_COS
REAL_INTEGRABLE_SIN_CX
REAL_INTEGRABLE_SPIKE
REAL_INTEGRABLE_SPIKE_FINITE
REAL_INTEGRABLE_SPIKE_INTERIOR
REAL_INTEGRABLE_SPIKE_SET
REAL_INTEGRABLE_SPIKE_SET_EQ
REAL_INTEGRABLE_STRADDLE
REAL_INTEGRABLE_STRETCH
REAL_INTEGRABLE_SUB
REAL_INTEGRABLE_SUBINTERVAL
REAL_INTEGRABLE_SUM
REAL_INTEGRABLE_UNIFORM_LIMIT
REAL_INTEGRAL
REAL_INTEGRAL_0
REAL_INTEGRAL_ABS_BOUND_INTEGRAL
REAL_INTEGRAL_ADD
REAL_INTEGRAL_COMBINE
REAL_INTEGRAL_CONST
REAL_INTEGRAL_COS_NX
REAL_INTEGRAL_DIRICHLET_KERNEL_MUL_EXPAND
REAL_INTEGRAL_EMPTY
REAL_INTEGRAL_EQ
REAL_INTEGRAL_EQ_0
REAL_INTEGRAL_EQ_HAS_INTEGRAL
REAL_INTEGRAL_HAS_REAL_DERIVATIVE
REAL_INTEGRAL_LBOUND
REAL_INTEGRAL_LE
REAL_INTEGRAL_LINEAR
REAL_INTEGRAL_LMUL
REAL_INTEGRAL_NEG
REAL_INTEGRAL_NULL
REAL_INTEGRAL_OPEN_INTERVAL
REAL_INTEGRAL_PERIODIC_OFFSET
REAL_INTEGRAL_POS
REAL_INTEGRAL_REAL_MEASURE
REAL_INTEGRAL_REAL_MEASURE_UNIV
REAL_INTEGRAL_REFL
REAL_INTEGRAL_REFLECT
REAL_INTEGRAL_REFLECT_AND_ADD
REAL_INTEGRAL_RESTRICT
REAL_INTEGRAL_RESTRICT_INTER
REAL_INTEGRAL_RESTRICT_UNIV
REAL_INTEGRAL_RMUL
REAL_INTEGRAL_SIN_AND_COS
REAL_INTEGRAL_SIN_NX
REAL_INTEGRAL_SIN_OVER_X_BOUND
REAL_INTEGRAL_SPIKE
REAL_INTEGRAL_SPIKE_SET
REAL_INTEGRAL_SUB
REAL_INTEGRAL_SUBSET_LE
REAL_INTEGRAL_SUM
REAL_INTEGRAL_TWEAK_ENDS
REAL_INTEGRAL_UBOUND
REAL_INTEGRAL_UNIQUE
REAL_INTERVAL_EQ_EMPTY
REAL_INTERVAL_INTERVAL
REAL_INTERVAL_NE_EMPTY
REAL_INTERVAL_OPEN_SUBSET_CLOSED
REAL_INTERVAL_SING
REAL_INTERVAL_TRANSLATION
REAL_INV
REAL_INV1
REAL_INV2
REAL_INVINV
REAL_INV_1
REAL_INV_1_LE
REAL_INV_1_LT
REAL_INV_DIV
REAL_INV_EQ
REAL_INV_EQ_0
REAL_INV_EQ_1
REAL_INV_INV
REAL_INV_LE_1
REAL_INV_LT
REAL_INV_LT1
REAL_INV_LT_1
REAL_INV_MUL
REAL_INV_MUL_WEAK
REAL_INV_NEG
REAL_INV_POS
REAL_INV_POW
REAL_INV_RPOW
REAL_IVT_DECREASING
REAL_IVT_INCREASING
REAL_LE
REAL_LE1_POW2
REAL_LEBESGUE_MEASURABLE
REAL_LEBESGUE_MEASURABLE_CLOSED
REAL_LEBESGUE_MEASURABLE_COMPACT
REAL_LEBESGUE_MEASURABLE_COMPL
REAL_LEBESGUE_MEASURABLE_COUNTABLE_INTERS
REAL_LEBESGUE_MEASURABLE_COUNTABLE_INTERS_EXPLICIT
REAL_LEBESGUE_MEASURABLE_COUNTABLE_UNIONS
REAL_LEBESGUE_MEASURABLE_COUNTABLE_UNIONS_EXPLICIT
REAL_LEBESGUE_MEASURABLE_DIFF
REAL_LEBESGUE_MEASURABLE_EMPTY
REAL_LEBESGUE_MEASURABLE_IFF_MEASURABLE
REAL_LEBESGUE_MEASURABLE_INTER
REAL_LEBESGUE_MEASURABLE_INTERS
REAL_LEBESGUE_MEASURABLE_INTERVAL
REAL_LEBESGUE_MEASURABLE_ON_SUBINTERVALS
REAL_LEBESGUE_MEASURABLE_OPEN
REAL_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED
REAL_LEBESGUE_MEASURABLE_PREIMAGE_OPEN
REAL_LEBESGUE_MEASURABLE_UNION
REAL_LEBESGUE_MEASURABLE_UNIONS
REAL_LEBESGUE_MEASURABLE_UNIV
REAL_LET_ADD
REAL_LET_ADD2
REAL_LET_ANTISYM
REAL_LET_TOTAL
REAL_LET_TRANS
REAL_LE_01
REAL_LE_1_POW2
REAL_LE_ABS_MUL
REAL_LE_ABS_SINH
REAL_LE_ADD
REAL_LE_ADD2
REAL_LE_ADDL
REAL_LE_ADDR
REAL_LE_AFFINITY
REAL_LE_BETWEEN
REAL_LE_CASES_INTEGERS
REAL_LE_DIV
REAL_LE_DIV2_EQ
REAL_LE_DOUBLE
REAL_LE_FLOOR
REAL_LE_IM_DIV_CYCLIC
REAL_LE_INF
REAL_LE_INF_FINITE
REAL_LE_INF_SUBSET
REAL_LE_INTEGERS
REAL_LE_INV
REAL_LE_INV2
REAL_LE_INV_EQ
REAL_LE_LADD
REAL_LE_LCANCEL_IMP
REAL_LE_LDIV
REAL_LE_LDIV_EQ
REAL_LE_LINV
REAL_LE_LMUL
REAL_LE_LMUL_EQ
REAL_LE_LMUL_IMP
REAL_LE_LMUL_LOCAL
REAL_LE_LNEG
REAL_LE_LSQRT
REAL_LE_LT
REAL_LE_MAX
REAL_LE_MIN
REAL_LE_MUL
REAL_LE_MUL2
REAL_LE_MUL2V
REAL_LE_MUL3
REAL_LE_MUL_EQ
REAL_LE_NEG
REAL_LE_NEG2
REAL_LE_NEGL
REAL_LE_NEGR
REAL_LE_NEGTOTAL
REAL_LE_POW2
REAL_LE_POW_2
REAL_LE_RADD
REAL_LE_RCANCEL_IMP
REAL_LE_RDIV
REAL_LE_RDIV_EQ
REAL_LE_REFL
REAL_LE_REVERSE_INTEGERS
REAL_LE_RINV
REAL_LE_RMUL
REAL_LE_RMUL_EQ
REAL_LE_RMUL_IMP
REAL_LE_RNEG
REAL_LE_ROOT
REAL_LE_RSQRT
REAL_LE_SETDIST
REAL_LE_SETDIST_EQ
REAL_LE_SQUARE
REAL_LE_SQUARE_ABS
REAL_LE_SQUARE_POW
REAL_LE_SUB_LADD
REAL_LE_SUB_RADD
REAL_LE_SUC_POW2
REAL_LE_SUP_FINITE
REAL_LE_TOTAL
REAL_LE_TRANS
REAL_LE_X_SINH
REAL_LIM
REAL_LIM_SEQUENTIALLY
REAL_LINV_UNIQ
REAL_LNEG_UNIQ
REAL_LSQRT_LE
REAL_LT
REAL_LT1_POW2
REAL_LTE_ADD
REAL_LTE_ADD2
REAL_LTE_ANTISYM
REAL_LTE_TOTAL
REAL_LTE_TRANS
REAL_LT_01
REAL_LT_1
REAL_LT_1_POW2
REAL_LT_ADD
REAL_LT_ADD1
REAL_LT_ADD2
REAL_LT_ADDL
REAL_LT_ADDNEG
REAL_LT_ADDNEG2
REAL_LT_ADDR
REAL_LT_ADD_SUB
REAL_LT_AFFINITY
REAL_LT_ANTISYM
REAL_LT_BETWEEN
REAL_LT_DIV
REAL_LT_DIV2_EQ
REAL_LT_EXISTS
REAL_LT_FRACTION
REAL_LT_FRACTION_0
REAL_LT_GT
REAL_LT_HALF1
REAL_LT_HALF2
REAL_LT_IMP_LE
REAL_LT_IMP_NE
REAL_LT_IMP_NZ
REAL_LT_INF_FINITE
REAL_LT_INTEGERS
REAL_LT_INV
REAL_LT_INV2
REAL_LT_INV_EQ
REAL_LT_LADD
REAL_LT_LADD_IMP
REAL_LT_LCANCEL_IMP
REAL_LT_LDIV_EQ
REAL_LT_LE
REAL_LT_LINV
REAL_LT_LMUL
REAL_LT_LMUL_0
REAL_LT_LMUL_EQ
REAL_LT_LMUL_IMP
REAL_LT_LNEG
REAL_LT_LSQRT
REAL_LT_MAX
REAL_LT_MIN
REAL_LT_MUL
REAL_LT_MUL2
REAL_LT_MUL2_ALT
REAL_LT_MULTIPLE
REAL_LT_MUL_EQ
REAL_LT_NEG
REAL_LT_NEG2
REAL_LT_NEGTOTAL
REAL_LT_NZ
REAL_LT_POW2
REAL_LT_RADD
REAL_LT_RCANCEL_IMP
REAL_LT_RDIV
REAL_LT_RDIV_0
REAL_LT_RDIV_EQ
REAL_LT_REFL
REAL_LT_RINV
REAL_LT_RMUL
REAL_LT_RMUL_0
REAL_LT_RMUL_EQ
REAL_LT_RMUL_IMP
REAL_LT_RNEG
REAL_LT_RSQRT
REAL_LT_SQUARE
REAL_LT_SQUARE_ABS
REAL_LT_SUB_LADD
REAL_LT_SUB_RADD
REAL_LT_SUP_FINITE
REAL_LT_TOTAL
REAL_LT_TRANS
REAL_MAX_ACI
REAL_MAX_ASSOC
REAL_MAX_LE
REAL_MAX_LT
REAL_MAX_MAX
REAL_MAX_MIN
REAL_MAX_RPOW
REAL_MAX_SUP
REAL_MAX_SYM
REAL_MEAN
REAL_MEASURABLE
REAL_MEASURABLE_ALMOST
REAL_MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_ABSOLUTELY_INTEGRABLE
REAL_MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_INTEGRABLE
REAL_MEASURABLE_COMPACT
REAL_MEASURABLE_COUNTABLE_INTERS
REAL_MEASURABLE_COUNTABLE_UNIONS
REAL_MEASURABLE_COUNTABLE_UNIONS_BOUNDED
REAL_MEASURABLE_COUNTABLE_UNIONS_STRONG
REAL_MEASURABLE_DIFF
REAL_MEASURABLE_EMPTY
REAL_MEASURABLE_IMP_REAL_LEBESGUE_MEASURABLE
REAL_MEASURABLE_INNER_OUTER
REAL_MEASURABLE_INTER
REAL_MEASURABLE_MEASURABLE
REAL_MEASURABLE_NESTED_UNIONS
REAL_MEASURABLE_ON_0
REAL_MEASURABLE_ON_ABS
REAL_MEASURABLE_ON_ADD
REAL_MEASURABLE_ON_CASES
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_0
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET_0
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_OPEN_INTERVAL
REAL_MEASURABLE_ON_CONST
REAL_MEASURABLE_ON_DECREASING
REAL_MEASURABLE_ON_DECREASING_UNIV
REAL_MEASURABLE_ON_DIV
REAL_MEASURABLE_ON_INCREASING
REAL_MEASURABLE_ON_INCREASING_UNIV
REAL_MEASURABLE_ON_INV
REAL_MEASURABLE_ON_LEBESGUE_MEASURABLE_SUBSET
REAL_MEASURABLE_ON_LIMIT
REAL_MEASURABLE_ON_LMUL
REAL_MEASURABLE_ON_MAX
REAL_MEASURABLE_ON_MEASURABLE_SUBSET
REAL_MEASURABLE_ON_MIN
REAL_MEASURABLE_ON_MUL
REAL_MEASURABLE_ON_NEG
REAL_MEASURABLE_ON_NEG_EQ
REAL_MEASURABLE_ON_PREIMAGE_CLOSED
REAL_MEASURABLE_ON_PREIMAGE_CLOSED_INTERVAL
REAL_MEASURABLE_ON_PREIMAGE_OPEN
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_GE
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_GT
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_LE
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_LT
REAL_MEASURABLE_ON_PREIMAGE_OPEN_INTERVAL
REAL_MEASURABLE_ON_RESTRICT
REAL_MEASURABLE_ON_RMUL
REAL_MEASURABLE_ON_SIMPLE_FUNCTION_LIMIT
REAL_MEASURABLE_ON_SPIKE_SET
REAL_MEASURABLE_ON_SUB
REAL_MEASURABLE_ON_UNIV
REAL_MEASURABLE_OPEN
REAL_MEASURABLE_REAL_INTEGRABLE
REAL_MEASURABLE_REAL_INTERVAL
REAL_MEASURABLE_REAL_MEASURE_EQ_0
REAL_MEASURABLE_REAL_MEASURE_POS_LT
REAL_MEASURABLE_REAL_NEGLIGIBLE_SYMDIFF
REAL_MEASURABLE_SCALING
REAL_MEASURABLE_SCALING_EQ
REAL_MEASURABLE_TRANSLATION
REAL_MEASURABLE_UNION
REAL_MEASURABLE_UNIONS
REAL_MEASURE_DIFF_SUBSET
REAL_MEASURE_DISJOINT_UNION
REAL_MEASURE_DISJOINT_UNIONS
REAL_MEASURE_DISJOINT_UNIONS_IMAGE
REAL_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG
REAL_MEASURE_EMPTY
REAL_MEASURE_EQ_0
REAL_MEASURE_MEASURE
REAL_MEASURE_POS_LE
REAL_MEASURE_REAL_INTEGRAL
REAL_MEASURE_REAL_INTEGRAL_UNIV
REAL_MEASURE_REAL_INTERVAL
REAL_MEASURE_REAL_NEGLIGIBLE_SYMDIFF
REAL_MEASURE_REAL_NEGLIGIBLE_UNION
REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS
REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS_IMAGE
REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS_IMAGE_STRONG
REAL_MEASURE_SCALING
REAL_MEASURE_SUBSET
REAL_MEASURE_TRANSLATION
REAL_MEASURE_UNION
REAL_MEASURE_UNIONS_LE
REAL_MEASURE_UNIONS_LE_IMAGE
REAL_MEASURE_UNION_LE
REAL_MEASURE_UNIQUE
REAL_MIDDLE1
REAL_MIDDLE2
REAL_MIN_ACI
REAL_MIN_ASSOC
REAL_MIN_INF
REAL_MIN_LE
REAL_MIN_LT
REAL_MIN_MAX
REAL_MIN_MIN
REAL_MIN_RPOW
REAL_MIN_SYM
REAL_MK_NN_SSQRT
REAL_MK_POS_ABS_'
REAL_MONOTONE_CONVERGENCE_DECREASING
REAL_MONOTONE_CONVERGENCE_INCREASING
REAL_MONOTONE_CONVERGENCE_INCREASING_AE
REAL_MONO_POW2
REAL_MUL
REAL_MULTIPLICATIVE
REAL_MULTIPLICATIVE_CONST
REAL_MULTIPLICATIVE_CONVOLUTION
REAL_MULTIPLICATIVE_DELTA
REAL_MULTIPLICATIVE_DIVISORSUM
REAL_MULTIPLICATIVE_IGNOREZERO
REAL_MULTIPLICATIVE_MOBIUS
REAL_MUL_2
REAL_MUL_AC
REAL_MUL_COS_COS
REAL_MUL_COS_SIN
REAL_MUL_CX
REAL_MUL_DIV_ASSOC
REAL_MUL_GT
REAL_MUL_LINV_UNIQ
REAL_MUL_LNEG
REAL_MUL_LT
REAL_MUL_LTIMES
REAL_MUL_LTIMES_LE
REAL_MUL_LZERO
REAL_MUL_NN
REAL_MUL_POS_LE
REAL_MUL_POS_LT
REAL_MUL_RDIV
REAL_MUL_RID
REAL_MUL_RINV
REAL_MUL_RINV_UNIQ
REAL_MUL_RNEG
REAL_MUL_RSUM0
REAL_MUL_RTIMES
REAL_MUL_RTIMES_LE
REAL_MUL_RZERO
REAL_MUL_SIN_COS
REAL_MUL_SIN_SIN
REAL_MUL_SUM
REAL_MUL_SUM_NUMSEG
REAL_MVT
REAL_MVT_CAUCHY
REAL_MVT_SIMPLE
REAL_MVT_VERY_SIMPLE
REAL_NDIV_LEMMA1a
REAL_NDIV_LEMMA1b
REAL_NDIV_LEMMA2
REAL_NDIV_LEMMA3
REAL_NEG
REAL_NEGLIGIBLE_COUNTABLE
REAL_NEGLIGIBLE_COUNTABLE_UNIONS
REAL_NEGLIGIBLE_DIFF
REAL_NEGLIGIBLE_EMPTY
REAL_NEGLIGIBLE_FINITE
REAL_NEGLIGIBLE_FRONTIER_INTERVAL
REAL_NEGLIGIBLE_INSERT
REAL_NEGLIGIBLE_INTER
REAL_NEGLIGIBLE_ON_INTERVALS
REAL_NEGLIGIBLE_OUTER
REAL_NEGLIGIBLE_OUTER_LE
REAL_NEGLIGIBLE_REAL_INTERVAL
REAL_NEGLIGIBLE_SING
REAL_NEGLIGIBLE_SUBSET
REAL_NEGLIGIBLE_TRANSLATION
REAL_NEGLIGIBLE_TRANSLATION_EQ
REAL_NEGLIGIBLE_TRANSLATION_REV
REAL_NEGLIGIBLE_UNION
REAL_NEGLIGIBLE_UNIONS
REAL_NEGLIGIBLE_UNION_EQ
REAL_NEGNEG
REAL_NEG_0
REAL_NEG_ADD
REAL_NEG_DIV
REAL_NEG_EQ
REAL_NEG_EQ0
REAL_NEG_EQ_0
REAL_NEG_GE0
REAL_NEG_GT0
REAL_NEG_LE0
REAL_NEG_LMUL
REAL_NEG_LT0
REAL_NEG_MINUS1
REAL_NEG_MUL2
REAL_NEG_NEG
REAL_NEG_NZ
REAL_NEG_RMUL
REAL_NEG_SUB
REAL_NORM
REAL_NORM_POS
REAL_NOT_EQ
REAL_NOT_LE
REAL_NOT_LT
REAL_NUM_LE_0
REAL_NUM_ROUND
REAL_NZ_IMP_LT
REAL_OF_INT_OF_REAL
REAL_OF_NUM_BINOM
REAL_OF_NUM_GE
REAL_OF_NUM_GT
REAL_OF_NUM_ISUM
REAL_OF_NUM_ISUM_NUMSEG
REAL_OF_NUM_LT
REAL_OF_NUM_MAX
REAL_OF_NUM_MIN
REAL_OF_NUM_POW
REAL_OF_NUM_SUB
REAL_OF_NUM_SUC
REAL_OF_NUM_SUM
REAL_OF_NUM_SUM_NUMSEG
REAL_OPEN
REAL_OPEN_CLOSED_INTERVAL
REAL_OPEN_DIFF
REAL_OPEN_EMPTY
REAL_OPEN_EXISTS_RATIONAL
REAL_OPEN_HALFSPACE_GT
REAL_OPEN_HALFSPACE_LT
REAL_OPEN_IN
REAL_OPEN_INTER
REAL_OPEN_INTERS
REAL_OPEN_RATIONAL
REAL_OPEN_REAL_CLOSED
REAL_OPEN_REAL_INTERVAL
REAL_OPEN_SET_EXISTS_RATIONAL
REAL_OPEN_SET_RATIONAL
REAL_OPEN_SUBREAL_OPEN
REAL_OPEN_UNION
REAL_OPEN_UNIONS
REAL_OPEN_UNIV
REAL_OPPSIGN
REAL_OPPSIGN_LEMMA
REAL_PARTIAL_SUMS_LE_INFSUM
REAL_PERIODIC_INTEGER_MULTIPLE
REAL_POLYFUN_EQ_0
REAL_POLYFUN_EQ_CONST
REAL_POLYFUN_FINITE_ROOTS
REAL_POLYFUN_HAS_POSITIVE_ROOT
REAL_POLYFUN_ROOTBOUND
REAL_POLYFUN_SGN_AT_INFINITY
REAL_POLY_DIFF_EXPLICIT
REAL_POS
REAL_POSSQ
REAL_POS_ABS_MIDDLE
REAL_POS_NZ
REAL_POW
REAL_POW2_ABS
REAL_POW2_CLAUSES
REAL_POW2_THM
REAL_POWER_SERIES_CONV_IMP_ABSCONV
REAL_POW_1
REAL_POW_1_LE
REAL_POW_1_LT
REAL_POW_2_LE
REAL_POW_2_LT
REAL_POW_ADD
REAL_POW_DIV
REAL_POW_EQ
REAL_POW_EQ_0
REAL_POW_EQ_1
REAL_POW_EQ_1_IMP
REAL_POW_EQ_ABS
REAL_POW_EQ_EQ
REAL_POW_EQ_ODD
REAL_POW_EQ_ODD_EQ
REAL_POW_INV
REAL_POW_LBOUND
REAL_POW_LE
REAL_POW_LE2
REAL_POW_LE2_ODD
REAL_POW_LE2_ODD_EQ
REAL_POW_LE2_REV
REAL_POW_LE_1
REAL_POW_LT
REAL_POW_LT2
REAL_POW_LT2_ODD
REAL_POW_LT2_ODD_EQ
REAL_POW_LT2_REV
REAL_POW_LT_1
REAL_POW_MONO
REAL_POW_MONO_INV
REAL_POW_MONO_LT
REAL_POW_MUL
REAL_POW_NEG
REAL_POW_NZ
REAL_POW_ONE
REAL_POW_POW
REAL_POW_ROOT
REAL_POW_SUB
REAL_POW_ZERO
REAL_PROP_LE_LABS
REAL_PROP_LE_RABS
REAL_PROP_NN_LCANCEL
REAL_PROP_NN_POS
REAL_PROP_NN_RCANCEL
REAL_PROP_NZ_ABS
REAL_RAT_ABS_MIDDLE
REAL_RDISTRIB
REAL_RINV_2
REAL_RNEG_UNIQ
REAL_ROLLE
REAL_ROLLE_SIMPLE
REAL_ROOT_DIV
REAL_ROOT_INV
REAL_ROOT_LE
REAL_ROOT_MUL
REAL_ROOT_POW
REAL_ROOT_RPOW
REAL_RSQRT_LE
REAL_SECOND_MEAN_VALUE_THEOREM
REAL_SECOND_MEAN_VALUE_THEOREM_BONNET
REAL_SECOND_MEAN_VALUE_THEOREM_BONNET_FULL
REAL_SECOND_MEAN_VALUE_THEOREM_FULL
REAL_SECOND_MEAN_VALUE_THEOREM_GEN
REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL
REAL_SEGMENT
REAL_SEGMENT_INTERVAL
REAL_SEGMENT_SEGMENT
REAL_SEQ_OFFSET
REAL_SEQ_OFFSET_REV
REAL_SERIES
REAL_SERIES_0
REAL_SERIES_ABSCONV_IMP_CONV
REAL_SERIES_ADD
REAL_SERIES_CAUCHY
REAL_SERIES_CAUCHY_UNIFORM
REAL_SERIES_COMPARISON
REAL_SERIES_COMPARISON_UNIFORM
REAL_SERIES_DIFFS
REAL_SERIES_DIRICHLET
REAL_SERIES_FINITE
REAL_SERIES_FINITE_SUPPORT
REAL_SERIES_FROM
REAL_SERIES_GOESTOZERO
REAL_SERIES_LMUL
REAL_SERIES_NEG
REAL_SERIES_RATIO
REAL_SERIES_RESTRICT
REAL_SERIES_RMUL
REAL_SERIES_SUB
REAL_SERIES_SUBSET
REAL_SERIES_SUM
REAL_SERIES_TRIVIAL
REAL_SERIES_UNIQUE
REAL_SGN
REAL_SGN_0
REAL_SGN_ABS
REAL_SGN_CASES
REAL_SGN_DIV
REAL_SGN_EQ
REAL_SGN_IM_COMPLEX_DIV
REAL_SGN_INEQS
REAL_SGN_INV
REAL_SGN_MUL
REAL_SGN_NEG
REAL_SGN_RE_COMPLEX_DIV
REAL_SGN_SIN_AZIM
REAL_SIN
REAL_SIN_X2_ZEROS
REAL_SOS_EQ_0
REAL_SSQRT_CHAR
REAL_SSQRT_EQ_0
REAL_SSQRT_MONO
REAL_SSQRT_NEG
REAL_SSQRT_NN
REAL_SSQRT_SQUARE
REAL_SSQRT_SQUARE'
REAL_STEINHAUS
REAL_STONE_WEIERSTRASS
REAL_STONE_WEIERSTRASS_ALT
REAL_SUB
REAL_SUB_0
REAL_SUB_ABS
REAL_SUB_ADD
REAL_SUB_ADD2
REAL_SUB_ARG
REAL_SUB_COS
REAL_SUB_INV
REAL_SUB_INV2
REAL_SUB_LDISTRIB
REAL_SUB_LE
REAL_SUB_LNEG
REAL_SUB_LT
REAL_SUB_LZERO
REAL_SUB_NEG2
REAL_SUB_POLYFUN
REAL_SUB_POLYFUN_ALT
REAL_SUB_POW
REAL_SUB_POW_L1
REAL_SUB_POW_R1
REAL_SUB_RDISTRIB
REAL_SUB_REFL
REAL_SUB_RNEG
REAL_SUB_RZERO
REAL_SUB_SIN
REAL_SUB_SUB
REAL_SUB_SUB2
REAL_SUB_SUM0
REAL_SUB_TAN
REAL_SUB_TRIANGLE
REAL_SUMMABLE
REAL_SUMMABLE_0
REAL_SUMMABLE_ADD
REAL_SUMMABLE_COMPARISON
REAL_SUMMABLE_COMPLEX
REAL_SUMMABLE_EQ
REAL_SUMMABLE_EQ_COFINITE
REAL_SUMMABLE_EQ_EVENTUALLY
REAL_SUMMABLE_FROM_ELSEWHERE
REAL_SUMMABLE_GP
REAL_SUMMABLE_IFF
REAL_SUMMABLE_IFF_COFINITE
REAL_SUMMABLE_IFF_EVENTUALLY
REAL_SUMMABLE_IMP_BOUNDED
REAL_SUMMABLE_IMP_REAL_SUMS_BOUNDED
REAL_SUMMABLE_IMP_TOZERO
REAL_SUMMABLE_LMUL
REAL_SUMMABLE_NEG
REAL_SUMMABLE_RESTRICT
REAL_SUMMABLE_RMUL
REAL_SUMMABLE_SUB
REAL_SUMMABLE_SUBSET
REAL_SUMMABLE_TRIVIAL
REAL_SUMS
REAL_SUMSQ
REAL_SUMS_COMPLEX
REAL_SUMS_EQ
REAL_SUMS_FINITE_DIFF
REAL_SUMS_FINITE_UNION
REAL_SUMS_GP
REAL_SUMS_IFF
REAL_SUMS_IM
REAL_SUMS_INFSUM
REAL_SUMS_LE2
REAL_SUMS_OFFSET
REAL_SUMS_OFFSET_REV
REAL_SUMS_RE
REAL_SUMS_REINDEX
REAL_SUMS_SUMMABLE
REAL_SUM_INTEGRAL_BOUNDS_DECREASING
REAL_SUM_INTEGRAL_BOUNDS_INCREASING
REAL_SUM_INTEGRAL_LBOUND_DECREASING
REAL_SUM_INTEGRAL_LBOUND_INCREASING
REAL_SUM_INTEGRAL_UBOUND_DECREASING
REAL_SUM_INTEGRAL_UBOUND_INCREASING
REAL_SUM_OF_SQUARES
REAL_SUM_SQUARE_POS
REAL_SUP
REAL_SUP_ASCLOSE
REAL_SUP_BOUNDS
REAL_SUP_EQ_INF
REAL_SUP_EXISTS
REAL_SUP_LE
REAL_SUP_LE_FINITE
REAL_SUP_LE_SUBSET
REAL_SUP_LT_FINITE
REAL_SUP_UBOUND
REAL_SUP_UBOUND_LE
REAL_SUP_UNIQUE
REAL_SV_SSQRT_0
REAL_TAN
REAL_TAYLOR
REAL_TAYLOR_MVT_NEG
REAL_TAYLOR_MVT_POS
REAL_TENDSTO
REAL_TIETZE_PERIODIC_INTERVAL
REAL_TRIANGLE
REAL_TRUNCATE
REAL_TRUNCATE_POS
REAL_UNIFORMLY_CONTINUOUS_IMP_REAL_CONTINUOUS
REAL_UNIFORMLY_CONTINUOUS_ON
REAL_UNIFORMLY_CONTINUOUS_ON_ADD
REAL_UNIFORMLY_CONTINUOUS_ON_COMPOSE
REAL_UNIFORMLY_CONTINUOUS_ON_CONST
REAL_UNIFORMLY_CONTINUOUS_ON_ID
REAL_UNIFORMLY_CONTINUOUS_ON_LMUL
REAL_UNIFORMLY_CONTINUOUS_ON_NEG
REAL_UNIFORMLY_CONTINUOUS_ON_RMUL
REAL_UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY
REAL_UNIFORMLY_CONTINUOUS_ON_SUB
REAL_UNIFORMLY_CONTINUOUS_ON_SUBSET
REAL_UNIFORMLY_CONTINUOUS_ON_SUM
REAL_VARIATION_AFFINITY
REAL_VARIATION_AFFINITY2
REAL_VARIATION_COMBINE
REAL_VARIATION_CONTINUOUS
REAL_VARIATION_CONTINUOUS_LEFT
REAL_VARIATION_CONTINUOUS_RIGHT
REAL_VARIATION_GE_ABS_FUNCTION
REAL_VARIATION_GE_FUNCTION
REAL_VARIATION_MINUS_FUNCTION_MONOTONE
REAL_VARIATION_MONOTONE
REAL_VARIATION_NEG
REAL_VARIATION_POS_LE
REAL_VARIATION_REFLECT
REAL_VARIATION_REFLECT2
REAL_VARIATION_REFLECT_INTERVAL
REAL_VARIATION_TRANSLATION
REAL_VARIATION_TRANSLATION2
REAL_VARIATION_TRANSLATION_INTERVAL
REAL_VARIATION_TRIANGLE
REAL_VSUM
REAL_WLOG_LE
REAL_WLOG_LT
RECIPROCITY_LEGENDRE
RECIPROCITY_SET_LEMMA
RECIPROCITY_SIMPLE
RECTIFIABLE_PATH_DIFFERENTIABLE
RECTIFIABLE_PATH_IMP_PATH
RECTIFIABLE_PATH_JOIN
RECTIFIABLE_PATH_JOIN_EQ
RECTIFIABLE_PATH_JOIN_IMP
RECTIFIABLE_PATH_LINEPATH
RECTIFIABLE_PATH_REVERSEPATH
RECTIFIABLE_PATH_SUBPATH
RECTIFIABLE_VALID_PATH
RECT_INTERVAL
RECURRENCE_BERNPOLY
RECURSION_CASEWISE
RECURSION_CASEWISE_PAIRWISE
REDUCED_LABELLING
REDUCED_LABELLING_0
REDUCED_LABELLING_1
REDUCED_LABELLING_SUC
REDUCED_LABELLING_UNIQUE
REDUCE_LABELLING_0
REDUCE_POLY_SIMPLE
REFINES_CORRECT
REFINES_REFL
REFINES_SPECIFICATION
REFINES_TRANS
REFINES_WHILE
REFLECT2D_COMPOSE
REFLECT_ACROSS_COMPOSE
REFLECT_ACROSS_COMPOSE_ANGLE
REFLECT_ACROSS_COMPOSE_INVOLUTION
REFLECT_ACROSS_SYM
REFLECT_ALONG_0
REFLECT_ALONG_1D
REFLECT_ALONG_ADD
REFLECT_ALONG_BASIS
REFLECT_ALONG_EQ_0
REFLECT_ALONG_EQ_SELF
REFLECT_ALONG_INVOLUTION
REFLECT_ALONG_LINEAR_IMAGE
REFLECT_ALONG_MUL
REFLECT_ALONG_REFL
REFLECT_ALONG_SCALE
REFLECT_ALONG_ZERO
REFLECT_INJ
REFLECT_INTERVAL
REFLECT_REAL_INTERVAL
REFL_CLAUSE
REFL_correct
RELATIVE_BOUNDARY_OF_CONVEX_HULL
RELATIVE_BOUNDARY_OF_POLYHEDRON
RELATIVE_BOUNDARY_OF_TRIANGLE
RELATIVE_BOUNDARY_RETRACT_OF_PUNCTURED_AFFINE_HULL
RELATIVE_FRONTIER_BALL
RELATIVE_FRONTIER_CBALL
RELATIVE_FRONTIER_CLOSURE
RELATIVE_FRONTIER_CONVEX_HULL_CASES
RELATIVE_FRONTIER_CONVEX_HULL_EXPLICIT
RELATIVE_FRONTIER_CONVEX_INTER_AFFINE
RELATIVE_FRONTIER_EMPTY
RELATIVE_FRONTIER_EQ_EMPTY
RELATIVE_FRONTIER_FRONTIER
RELATIVE_FRONTIER_INJECTIVE_LINEAR_IMAGE
RELATIVE_FRONTIER_NONEMPTY_INTERIOR
RELATIVE_FRONTIER_NOT_SING
RELATIVE_FRONTIER_OF_CONVEX_HULL
RELATIVE_FRONTIER_OF_POLYHEDRON
RELATIVE_FRONTIER_OF_POLYHEDRON_ALT
RELATIVE_FRONTIER_OF_TRIANGLE
RELATIVE_FRONTIER_RETRACT_OF_PUNCTURED_AFFINE_HULL
RELATIVE_FRONTIER_SING
RELATIVE_FRONTIER_TRANSLATION
RELATIVE_INTERIOR
RELATIVE_INTERIOR_AFFINE
RELATIVE_INTERIOR_CONVEX_CONTAINS_SAME_RAY
RELATIVE_INTERIOR_CONVEX_HULL_EXPLICIT
RELATIVE_INTERIOR_CONVEX_INTER_AFFINE
RELATIVE_INTERIOR_CONVEX_PROLONG
RELATIVE_INTERIOR_EMPTY
RELATIVE_INTERIOR_EQ
RELATIVE_INTERIOR_EQ_CLOSURE
RELATIVE_INTERIOR_EQ_EMPTY
RELATIVE_INTERIOR_INJECTIVE_LINEAR_IMAGE
RELATIVE_INTERIOR_INTERIOR
RELATIVE_INTERIOR_LINEAR_IMAGE_CONVEX
RELATIVE_INTERIOR_MAXIMAL
RELATIVE_INTERIOR_NONEMPTY_INTERIOR
RELATIVE_INTERIOR_OF_POLYHEDRON
RELATIVE_INTERIOR_OPEN
RELATIVE_INTERIOR_OPEN_IN
RELATIVE_INTERIOR_PCROSS
RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT
RELATIVE_INTERIOR_PROLONG
RELATIVE_INTERIOR_SEGMENT
RELATIVE_INTERIOR_SING
RELATIVE_INTERIOR_SUBSET
RELATIVE_INTERIOR_TRANSLATION
RELATIVE_INTERIOR_UNBOUNDED_CONVEX_CONTAINS_RAY
RELATIVE_INTERIOR_UNBOUNDED_CONVEX_CONTAINS_RAYS
RELATIVE_INTERIOR_UNIQUE
RELATIVE_INTERIOR_UNIV
RELPOW
RELPOW_LEMMA
RELPOW_LEMMA_1
RELPOW_LEMMA_2
RELPOW_M
RELPOW_R
RELPOW_RTC
RELPOW_SEQUENCE
REMOVE
REMOVE_COL1
REMOVE_HD_COL
REMOVE_LAST
REM_FALSE
REM_NEQ
REM_NIL
REPLICATE
REP_ABS_PAIR
REST
RESTRICTED_ENSURES
RESTRICTED_EXISTS_TRANSITION
RESTRICTED_EXISTS_TRANSITION_STMT
RESTRICTED_LEADSTO
RESTRICTED_STABLE
RESTRICTED_STABLE_STMT
RESTRICTED_TRIPLE
RESTRICTED_UNLESS
RESTRICTED_UNLESS_STMT
RESULT
RETRACTION
RETRACTION_ARC
RETRACTION_IDEMPOTENT
RETRACTION_IMP_QUOTIENT_MAP
RETRACTION_REFL
RETRACTION_SUBSET
RETRACTION_o
RETRACT_FIXPOINT_PROPERTY
RETRACT_OF_CLOSED
RETRACT_OF_COHOMOTOPICALLY_TRIVIAL
RETRACT_OF_COHOMOTOPICALLY_TRIVIAL_NULL
RETRACT_OF_COMPACT
RETRACT_OF_CONNECTED
RETRACT_OF_CONTRACTIBLE
RETRACT_OF_EMPTY
RETRACT_OF_HOMOTOPICALLY_TRIVIAL
RETRACT_OF_HOMOTOPICALLY_TRIVIAL_NULL
RETRACT_OF_IMP_EXTENSIBLE
RETRACT_OF_IMP_SUBSET
RETRACT_OF_INJECTIVE_LINEAR_IMAGE
RETRACT_OF_LINEAR_IMAGE_EQ
RETRACT_OF_LOCALLY_COMPACT
RETRACT_OF_LOCALLY_CONNECTED
RETRACT_OF_LOCALLY_PATH_CONNECTED
RETRACT_OF_PATH_CONNECTED
RETRACT_OF_PCROSS
RETRACT_OF_REFL
RETRACT_OF_SIMPLY_CONNECTED
RETRACT_OF_SING
RETRACT_OF_SUBSET
RETRACT_OF_TRANS
RETRACT_OF_TRANSLATION
RETRACT_OF_TRANSLATION_EQ
REVERSE
REVERSEPATH_JOINPATHS
REVERSEPATH_LINEAR_IMAGE
REVERSEPATH_LINEPATH
REVERSEPATH_REVERSEPATH
REVERSEPATH_SUBPATH
REVERSEPATH_TRANSLATION
REVERSE_APPEND
REVERSE_LINEAR_IMAGE
REVERSE_REVERSE
REVERSE_TRANSLATION
REVPERM
REV_ASSOCD
REV_ASSOCD_FILTER
RE_ADD
RE_CACS
RE_CACS_BOUND
RE_CACS_BOUNDS
RE_CASN
RE_CASN_BOUND
RE_CASN_BOUNDS
RE_CATN_BOUNDS
RE_CCOS
RE_CEXP
RE_CLOG
RE_CLOG_POS_LE
RE_CLOG_POS_LT
RE_CLOG_POS_LT_IMP
RE_CMUL
RE_CNJ
RE_COMPLEX_DIV_EQ_0
RE_COMPLEX_DIV_GE_0
RE_COMPLEX_DIV_GT_0
RE_COMPLEX_DIV_LEMMA
RE_COMPLEX_DIV_LE_0
RE_COMPLEX_DIV_LT_0
RE_CSIN
RE_CSQRT
RE_CX
RE_DEF
RE_DIV_CX
RE_II
RE_LINEPATH_CX
RE_MUL_CX
RE_MUL_II
RE_NEG
RE_POS_SEGMENT
RE_POW_2
RE_SUB
RE_VSUM
RE_WINDING_NUMBER
RHS
RHS_4_BOUND_PRE
RHS_4_F5_LE_SUM
RHS_4_LT_ONE_MESSY
RIEMANN_LEBESGUE
RIEMANN_LEBESGUE_COS
RIEMANN_LEBESGUE_SIN
RIEMANN_LEBESGUE_SIN_HALF
RIEMANN_LEBESGUE_SQUARE_INTEGRABLE
RIEMANN_LOCALIZATION
RIEMANN_LOCALIZATION_INTEGRAL
RIEMANN_LOCALIZATION_INTEGRAL_RANGE
RIEMANN_LOCALIZATION_INTEGRAL_RANGE_HALF
RIEMANN_MAPPING_THEOREM
RIESZ_FISCHER
RIGHT_ADD_DISTRIB
RIGHT_AND_EXISTS_THM
RIGHT_AND_FORALL_TAG
RIGHT_AND_FORALL_THM
RIGHT_EXISTS_AND_THM
RIGHT_EXISTS_IMP_THM
RIGHT_FORALL_IMP_THM
RIGHT_FORALL_OR_THM
RIGHT_IMP_EXISTS_TAG
RIGHT_IMP_EXISTS_THM
RIGHT_IMP_FORALL_TAG
RIGHT_IMP_FORALL_THM
RIGHT_INVERSE_LINEAR
RIGHT_INVERTIBLE_TRANSP
RIGHT_OR_DISTRIB
RIGHT_OR_EXISTS_THM
RIGHT_OR_FORALL_TAG
RIGHT_OR_FORALL_THM
RIGHT_SUB_DISTRIB
RIGID_TRANSFORMATION_BETWEEN_2
RIGID_TRANSFORMATION_BETWEEN_3
RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS
RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS_STRONG
ROLLE
ROL_APPEND
ROL_APPEND2
ROL_APPEND_INSERT
ROL_CONS
ROL_CONS_CONS
ROL_CONS_CONS_DELETE
ROL_CONS_CONS_LT
ROL_INSERT_BACK_THM
ROL_INSERT_FRONT_THM
ROL_INSERT_THM
ROL_MEM
ROL_NIL
ROL_SING
ROL_SUBLIST
ROL_SUBLIST_LT
ROL_TAIL
ROOT_0
ROOT_1
ROOT_2
ROOT_DIV
ROOT_EXP_LOG
ROOT_INJ
ROOT_INV
ROOT_LN
ROOT_LT_LEMMA
ROOT_MONO_LE
ROOT_MONO_LE_EQ
ROOT_MONO_LT
ROOT_MONO_LT_EQ
ROOT_MUL
ROOT_NONPOWER
ROOT_POS_LE
ROOT_POS_LT
ROOT_POS_POSITIVE
ROOT_POS_UNIQ
ROOT_POW_POS
ROOT_UNIQUE
ROOT_WORKS
ROTATE2D_0
ROTATE2D_2PI
ROTATE2D_ADD
ROTATE2D_ADD_VECTORS
ROTATE2D_COMPLEX
ROTATE2D_EQ
ROTATE2D_EQ_0
ROTATE2D_NPI
ROTATE2D_PI
ROTATE2D_PI2
ROTATE2D_POLAR
ROTATE2D_SUB
ROTATE2D_SUB_ARG
ROTATE2D_ZERO
ROTATE_ABOUT_INVERT
ROTATE_EQ_REFLECT_LEMMA
ROTATE_EQ_REFLECT_PI_LEMMA
ROTATE_LIST_TO_FRONT_0
ROTATE_LIST_TO_FRONT_1
ROTATION_EXISTS
ROTATION_EXISTS_1
ROTATION_HORIZONTAL_LINE
ROTATION_HORIZONTAL_PLANE
ROTATION_LOWDIM_HORIZONTAL
ROTATION_MATRIX_2
ROTATION_MATRIX_EXISTS_BASIS
ROTATION_MATRIX_ROTATE2D
ROTATION_MATRIX_ROTATE2D_EQ
ROTATION_PLANE_HORIZONTAL
ROTATION_RIGHTWARD_LINE
ROTATION_ROTATE2D
ROTATION_ROTATE2D_EXISTS
ROTATION_ROTATE2D_EXISTS_GEN
ROTATION_ROTATE2D_EXISTS_ORTHOGONAL
ROTATION_ROTATE2D_EXISTS_ORTHOGONAL_ORIENTED
ROTHE
ROTOINVERSION_MATRIX_REFLECT_ALONG
ROUND_WORKS
ROWS_TRANSP
ROW_TRANSP
RPOW_1_LE
RPOW_ADD
RPOW_ADD_ALT
RPOW_EQ_0
RPOW_INV
RPOW_LE2
RPOW_LNEG
RPOW_LT2
RPOW_MONO
RPOW_MONO_INV
RPOW_MUL
RPOW_NEG
RPOW_ONE
RPOW_POS_LE
RPOW_POS_LT
RPOW_POW
RPOW_RPOW
RPOW_SQRT
RPOW_ZERO
RSA
RSC
RSC_CASES
RSC_CLOSED
RSC_IDEMP
RSC_INC
RSC_INC_RC
RSC_INC_SC
RSC_INDUCT
RSC_INV
RSC_MONO
RSC_REFL
RSC_SYM
RSQUAREFREE_DECOMP
RSQUAREFREE_ROOTS
RSTC
RSTC_CASES
RSTC_CASES_L
RSTC_CASES_R
RSTC_CLOSED
RSTC_IDEMP
RSTC_INC
RSTC_INC_RC
RSTC_INC_RSC
RSTC_INC_RTC
RSTC_INC_SC
RSTC_INC_STC
RSTC_INC_TC
RSTC_INDUCT
RSTC_INV
RSTC_MONO
RSTC_REFL
RSTC_RULES
RSTC_SYM
RSTC_TRANS
RSTC_TRANS_L
RSTC_TRANS_R
RSUM_BOUND
RSUM_COMPONENT_LE
RSUM_DIFF_BOUND
RTC
RTCP
RTC_CASES
RTC_CASES_L
RTC_CASES_R
RTC_CLOSED
RTC_CR
RTC_IDEMP
RTC_INC
RTC_INC_RC
RTC_INC_TC
RTC_INDUCT
RTC_INDUCT_L
RTC_INDUCT_R
RTC_INV
RTC_MONO
RTC_NE_IMP_TC
RTC_REFL
RTC_RELPOW
RTC_RULES
RTC_SIGMA
RTC_STUTTER
RTC_SYM
RTC_TC_LEMMA
RTC_TRANS
RTC_TRANS_L
RTC_TRANS_R
RTCpredn
RTCpredn_EQ_RTCredn
RTCpredn_RTCredn
RTCredn
RTCredn_RTCpredn
RTCredn_ap_monotonic
Ray_DEF
ReachLemma
RightAngle_DEF
r_scale_bij
r_scale_cont
r_scale_h
r_scale_hom
r_scale_inv
r_scale_point
r_scale_v
radicals
range
rank
rational
rcone_eq
rcone_ge
rcone_gt
rconesgn
re_Union
re_compl
re_intersect
re_null
re_subset
re_union
re_universe
reachable
reachableInvariant
reachableN
reachableNSymmetry
reachableN_CLAUSES
reachableN_Five
reachableN_Four
reachableN_One
reachableN_Three
reachableN_Two
real
real012
real_FINITE
real_INFINITE
real_abs
real_bounded
real_cases
real_closed
real_compact
real_continuous
real_continuous_at
real_continuous_atreal
real_continuous_on
real_continuous_within
real_continuous_withinreal
real_convex_on
real_derivative
real_differentiable
real_differentiable_on
real_div
real_div_assoc
real_div_denom
real_div_denom_lt
real_eq_div
real_finite_increase
real_ge
real_gt
real_half_EL
real_half_LE
real_half_LLE
real_half_LT
real_infsum
real_integrable_on
real_integral
real_interval
real_le
real_lebesgue_measurable
real_lt
real_max
real_measurable
real_measurable_on
real_measure
real_middle1_lt
real_middle2_lt
real_min
real_mod
real_multiplicative
real_negligible
real_open
real_ordered_list
real_pow
real_segment
real_sgn
real_sub
real_sub_half
real_summable
real_sums
real_tybij
real_uniformly_continuous_on
real_variation
reallim
rect
rectagon_2
rectagon_adj
rectagon_curve
rectagon_delete
rectagon_delete_end
rectagon_endpoint
rectagon_endpoint0
rectagon_graph_k33_false
rectagon_h_edge
rectagon_nonsing
rectagon_order
rectagon_rectangle_grid_sq
rectagon_segment
rectagon_subset
rectagon_subset_endpoint
rectagon_surround_conn2
rectagon_v_edge
rectagonal_graph_k33
rectangle_convex
rectangle_euclid
rectangle_grid_conn2
rectangle_grid_edge
rectangle_grid_h
rectangle_grid_h_conn2
rectangle_grid_sq
rectangle_grid_sq_cls
rectangle_grid_subset
rectangle_grid_v
rectangle_h
rectangle_inter
rectangle_lemma1
rectangle_lemma2
rectangle_lemma3
rectangle_lemma4
rectangle_lemma5
rectangle_lemma6
rectangle_open
rectangle_squ
rectangle_v
rectifiable_path
recursion_on_dyadic_rationals
recursion_on_dyadic_rationals_1
reduced
refines
reflA_BIJ
reflA_cont
reflA_edge
reflA_h_edge
reflA_homeo
reflA_pointI
reflA_segment
reflA_squ
reflA_v_edge
reflAf_inv
reflAi_inv
reflB_BIJ
reflB_cont
reflB_edge
reflB_h_edge
reflB_homeo
reflB_pointI
reflB_segment
reflB_squ
reflB_v_edge
reflBf_inv
reflBi_inv
reflC_BIJ
reflC_cont
reflC_edge
reflC_homeo
reflC_hv_edge
reflC_pointI
reflC_segment
reflC_squ
reflC_vh_edge
reflCf_inv
reflCi_inv
reflect2d
reflect_across
reflect_along
reflexive
relative_frontier
relative_interior
rep3_lt
repeating
replace_inj
replace_x
rest_eq_gt_lem
rest_eq_lt_lem
rest_gt_lem
rest_int_gt_lem
rest_int_lt_lem
rest_lt_lem
result_INDUCT,result_RECURSION
retract_of
retraction
retval
reversepath
reversion
right
right_left
robinson
root
rotate2d
rotate_about
rotation_matrix
rotoinversion_matrix
round
row
row_col
row_disj
rows
rowvector
rpow
rsquarefree
rsum
rthm2