FUN_EQ_THM
COND_ID
bool_RECURSION
PAIR_EQ
FORALL_PAIR_THM
num_RECURSION_STD
EQ_ADD_RCANCEL
ARITH_ADD_conjunct1
MULT_SYM
EQ_MULT_LCANCEL
MULT_AC_conjunct2
EXP_MULT
LT_0
LTE_ANTISYM
LT_CASES
NOT_LT
LE_ADD
LT_ADD_LCANCEL
LT_ADD2
LT_MULT_LCANCEL
num_MAX
ODD_ADD
EVEN_EXISTS
ADD_SUB
SUB_ADD_RCANCEL
Hypermap.ZR_LT_1
EXP_MONO_LE_IMP
DIVMOD_UNIQ
MOD_EQ
DIV_LT
DIV_EQ_0
DIV_MULT_ADD
SUB_ELIM_THM
TRANSITIVE_STEPWISE_LE
WF_SUBSET
MEASURE_LE
ARITH_PRE_conjunct1
ARITH_LE_conjunct0
ARITH_EVEN_conjunct3
ARITH_SUB_conjunct0
ARITH_MULT_conjunct0
ARITH_SUC_conjunct2
INJF_INJ
ALL2_conjunct0
ZIP_conjunct0
REVERSE_APPEND
LENGTH_EQ_NIL
MEM_APPEND
SURJECTIVE_MAP
EL_CONS
DIST_ADD2_REV
BOUNDS_IGNORE
NADD_EQ_TRANS
NADD_LE_ANTISYM
NADD_ADD_WELLDEF
NADD_MUL_ASSOC
NADD_EQ_IMP_LE
NADD_ARCH_ZERO
NADD_MUL_LINV_LEMMA0
NADD_MUL_LINV_LEMMA7
hreal_of_num_th
HREAL_LE_ADD_RCANCEL
HREAL_LE_ADD2
TREAL_OF_NUM_EQ
TREAL_ADD_SYM
TREAL_MUL_LID
TREAL_LE_LADD_IMP
TREAL_ADD_WELLDEF
real_of_num_th
REAL_COMPLETE
REAL_ADD_AC_conjunct2
REAL_POW_NEG
REAL_LET_TRANS
REAL_SUB_LT
REAL_ENTIRE
REAL_OF_NUM_GE
REAL_EQ_ADD_LCANCEL_0
REAL_NEG_MUL2
REAL_NOT_LE
REAL_LT_TOTAL
REAL_LT_ADD2
REAL_LT_ADD1
REAL_NEG_EQ_0
REAL_LT_ADDR
REAL_LE_SUB_LADD
REAL_LTE_ADD2
REAL_EQ_SUB_RADD
REAL_SUB_LDISTRIB
REAL_ABS_LE
REAL_ABS_SIGN2
REAL_BOUNDS_LT
REAL_MIN_SYM
REAL_MIN_LE
REAL_ABS_POW
REAL_MUL_LINV_UNIQ
REAL_INV_NEG
REAL_DIV_REFL
REAL_MUL_AC_conjunct1
REAL_POW_DIV
REAL_LE_RCANCEL_IMP
REAL_MUL_POS_LE
REAL_EQ_LDIV_EQ
REAL_LT_SQUARE
REAL_INV_LT_1
REAL_POW_LE2
REAL_POW_1_LT
REAL_LE_DIV
REAL_LT_SQUARE_ABS
REAL_POW_LT2_REV
REAL_POW_LE2_ODD
REAL_ARCH_LT
REAL_SGN
RAT_LEMMA1
dest_int_rep
int_mul_th
INT_IMAGE
INT_ABS_POS
INT_ADD_RID
INT_EQ_NEG2
INT_LE_LNEG
INT_LE_REFL
INT_LE_TRANS
INT_MUL_LID
INT_MUL_SYM
INT_NEG_MINUS1
INT_OF_NUM_EQ
INT_OF_NUM_MIN
INT_POW_1
REAL_SGN_EQ_conjunct0
INT_FORALL_POS
INT_GE
INT_DIVMOD_UNIQ
INT_GCD_EXISTS
IN_ELIM_THM_conjunct4
NOT_IN_EMPTY
IN_DIFF
EXISTS_IN_INSERT
SUBSET_TRANS
SUBSET_UNIV
PSUBSET_ALT
INTER_ASSOC
IN_DISJOINT
DIFF_EQ_EMPTY
INSERT_INSERT
DISJOINT_INSERT
DELETE_NON_ELEMENT
DELETE_INSERT
FORALL_IN_UNIONS
INTERS_UNION
IMAGE_ID
IMAGE_DELETE_INJ
EXISTS_SUBSET_IMAGE
IMAGE_UNIONS
UNIONS_IMAGE
INTERS_UNIONS
FINITE_UNION_IMP
FINITE_DELETE
FINITE_FINITE_PREIMAGE
FINITE_SUBSET_IMAGE
FINREC_UNIQUE_LEMMA
SUBSET_RESTRICT
CARD_UNION
HAS_SIZE_0
HAS_SIZE_CLAUSES_conjunct0
CARD_PSUBSET
CARD_IMAGE_INJ
CARD_IMAGE_EQ_INJ
FORALL_IN_GSPEC_conjunct0
FINITE_CROSS
FINITE_UNIONS
FINITE_NUMSEG_LT
num_INFINITE
LENGTH_LIST_OF_SET
SET_OF_LIST_EQ_EMPTY
CARD_SET_OF_LIST_LE
INJECTIVE_ON_LEFT_INVERSE
FUNCTION_FACTORS_LEFT
INJECTIVE_IMAGE
BIJECTIONS_HAS_SIZE_EQ
SUP
REAL_SUP_LT_FINITE
REAL_SUP_ASCLOSE
REAL_INF_LE_FINITE
REAL_INF_BOUNDS
INF_INSERT_FINITE
NUMSEG_REC
CARD_NUMSEG
FINITE_INDEX_NUMSEG
NUMSEG_LT
FINITE_SUPPORT
ITERATE_CLAUSES
ITERATE_SING
ITERATE_EQ
ITERATE_SUPERSET
NEUTRAL_ADD
NSUM_ADD
NSUM_LE
NSUM_EQ_0_IFF
NSUM_UNION_RZERO
CARD_EQ_NSUM
NSUM_LE_NUMSEG
NSUM_CLAUSES_NUMSEG_conjunct1
NEUTRAL_REAL_MUL
SUM_SUPPORT
SUM_CLAUSES_conjunct0
SUM_LT
SUM_POS_LE
SUM_SING
SUM_UNION_LZERO
SUM_BOUND_LT_GEN
SUM_MULTICOUNT_GEN
SUM_SUBSET_SIMPLE
SUM_UNION_NONZERO
SUM_CLOSED
SUM_CONST_NUMSEG
SUM_SWAP_NUMSEG
SUM_CLAUSES_NUMSEG_conjunct0
SUM_DIFFS
REAL_SUB_POLYFUN
DIMINDEX_UNIV
FINITE_INDEX_WORKS
LAMBDA_ETA
FSTCART_PASTECART
HAS_SIZE_1
IN_ELIM_PASTECART_THM
ADMISSIBLE_CONST
ADMISSIBLE_IMP_SUPERADMISSIBLE
WF_REC_CASES'
UNIONS_PRED
WOSET_REFL
WOSET
UNION_FL
LINSEG_FL
EXTEND_LINSEG
ORDINAL_UNION_LEMMA
ZL
FL_RESTRICTED_SUBSET
INJECTIVE_LEFT_INVERSE_NONEMPTY
CARD_LET_TRANS
CARD_LE_RELATIONAL
CARD_NOT_LT
CARD_EQ_CONG
CARD_INFINITE_CONG
CARD_EQ_CARD_IMP
CARD_EQ_IMAGE
CARD_LE_SQUARE
CARD_MUL_SYM
CARD_SQUARE_INFINITE
CARD_ADD_ABSORB_LE
CANTOR_THM_UNIV
COUNTABLE_RESTRICT
COUNTABLE_SING
COUNTABLE_AS_IMAGE
CARD_EQ_LIST
UNCOUNTABLE_REAL
UPPER_BOUND_FINITE_SET_REAL
APPROACHABLE_LT_LE
HULL_P
HULL_ANTIMONO
HULL_UNION_SUBSET
HULL_INC
REAL_ARCH_INV
FORALL_POS_MONO_1
POW_2_SQRT_ABS
FORALL_3
DOT_2
VECTOR_MUL_COMPONENT
VECTOR_ADD_RINV
VECTOR_MUL_LZERO
VECTOR_SUB_RDISTRIB
VECTOR_NEG_MINUS1
VECTOR_NEG_EQ_0
DOT_LADD
DOT_LNEG
DOT_POS_LT
CONNECTED_REAL_LEMMA
SQRT_MUL
SQRT_MONO_LT_EQ
REAL_LE_RSQRT
NORM_NEG
NORM_EQ_0_IMP
NORM_CAUCHY_SCHWARZ_ABS
COMPONENT_LE_NORM
NORM_LT
NORM_LE_SQUARE
DOT_NORM_SUB
DIST_TRIANGLE_ALT
DIST_TRIANGLE_HALF_R
NEUTRAL_VECTOR_ADD
VSUM_0
VSUM_COMPONENT
VSUM_NEG
VSUM_RESTRICT
VSUM_NORM_TRIANGLE
VSUM_GROUP
VSUM_VSUM_PRODUCT
VSUM_DIFFS_ALT
DOT_RSUM
VSUM_COMBINE_L
VSUM_PAIR
BASIS_INJ
DOT_BASIS_BASIS
ORTHOGONAL_0
ORTHOGONAL_BASIS_BASIS
VECTOR_3_conjunct2
LINEAR_COMPOSE_NEG
LINEAR_NEGATION
LINEAR_ADD
BILINEAR_LADD
BILINEAR_LZERO
BILINEAR_BOUNDED_POS
ADJOINT_ADJOINT
TRANSP_COMPONENT
MATRIX_ADD_RID
MATRIX_MUL_ASSOC
MATRIX_CMUL_LZERO
MATRIX_VECTOR_MUL_ADD_RDISTRIB
DOT_LMUL_MATRIX
ROW_TRANSP
MATRIX_MUL_DOT
MATRIX_WORKS
ADJOINT_MATRIX
NORM_BOUND_GENERALIZE
ONORM_COMPOSE
LIFT_DROP_conjunct0
FORALL_DROP_FUN
LIFT_SUB
DROP_ADD
DIST_LIFT
DROP_WLOG_LE
LINEAR_FSTCART
FSTCART_SUB
SNDCART_SUB
PASTECART_SUB
NORM_PASTECART_LE
SUBSPACE_0
SUBSPACE_LINEAR_IMAGE
SPAN_MONO
INDEPENDENT_MONO
SPAN_0
SPAN_SUB
SPAN_CLAUSES_conjunct2
SPAN_LINEAR_IMAGE
SPAN_SING
SPAN_TRANS
HAS_SIZE_STDBASIS
SPANNING_SUBSET_INDEPENDENT
INDEPENDENT_EXPLICIT
BASIS_SUBSPACE_EXISTS
DIM_LE_CARD
CARD_LE_DIM_SPANNING
DIM_EQ_CARD
DIM_INSERT
BASIS_ORTHOGONAL
LINEAR_EQ_0_SPAN
RIGHT_INVERTIBLE_TRANSP
MATRIX_LEFT_INVERTIBLE_INDEPENDENT_COLUMNS
LINEAR_SURJECTIVE_IFF_INJECTIVE
RIGHT_INVERSE_LINEAR
INVERTIBLE_RIGHT_INVERSE
DOT_ROWVECTOR_COLUMNVECTOR
SUBSPACE_ORTHOGONAL_TO_VECTOR
MATRIX_VECTOR_MUL_INJECTIVE_ON_ROWSPACE
RANK_DIM_IM
FULL_RANK_SURJECTIVE
RANK_0
LINEAR_SINGULAR_INTO_HYPERPLANE
PAIRWISE_ORTHOGONAL_INDEPENDENT
VECTOR_IN_ORTHOGONAL_SPANNINGSET
ORTHOGONAL_TO_SUBSPACE_EXISTS_GEN
ORTHOGONAL_SUBSPACE_DECOMP_EXISTS
SUBSPACE_HYPERPLANE
DIM_SUMS_INTER
NUMSEG_DIMINDEX_NONEMPTY
INFNORM_EQ_0
COMPONENT_LE_INFNORM
NORM_CAUCHY_SCHWARZ_EQ
COLLINEAR_EMPTY
COLLINEAR_LEMMA_ALT
COLLINEAR_3_TRANS
BETWEEN_TRANS_2
MIDPOINT_REFL
MIDPOINT_COLLINEAR
SURJECTIVE_SCALING
QUANTIFY_SURJECTION_THM
INVERSE_UNIQUE_o
SWAP_GALOIS
PERMUTES_INVERSES
PERMUTES_SUPERSET
PERMUTES_INSERT
ITERATE_PERMUTE
PERMUTATION_I
SWAPSEQ_INVERSE_EXISTS
SWAPSEQ_EVEN_EVEN
PERMUTATION_BIJECTIVE
PERMUTATION_COMPOSE_EQ_conjunct1
SIGN_COMPOSE
IMAGE_INVERSE_PERMUTATIONS
SUM_OVER_PERMUTATIONS_INSERT
REAL_LE_REVERSE_INTEGERS
INTEGER_POS
RATIONAL_INV
REAL_TRUNCATE_POS
REAL_FLOOR_LE
REAL_FRAC_POS_LT
FLOOR_POS_LE
CARD_INTSEG_INT
PRODUCT_ADD_SPLIT
PRODUCT_POS_LT_NUMSEG
PRODUCT_EQ_0
PRODUCT_MUL
PRODUCT_DIV
PRODUCT_PERMUTE
DET_DIAGONAL
DET_ROW_ADD
BOUNDED_FUNCTIONS_BIJECTIONS_2
DET_MUL
DET_EQ_0_RANK
CRAMER_MATRIX_RIGHT
MATRIX_INV_COFACTOR
PRODUCT_CLAUSES_NUMSEG_conjunct1
INTEGER_PRODUCT
ORTHOGONAL_MATRIX_ALT
MATRIX_MUL_RTRANSP_DOT_ROW
ORTHOGONAL_MATRIX_ORTHONORMAL_ROWS_SPAN
ORTHOGONAL_TRANSFORMATION_INJECTIVE
FINITE_INDEX_NUMSEG_SPECIAL
ROTATION_MATRIX_EXISTS_BASIS
UNION_UNIV_conjunct0
TOPOLOGY_EQ
OPEN_IN_UNION
CLOSED_IN_SUBSET
OPEN_IN_CLOSED_IN_EQ
TOPSPACE_SUBTOPOLOGY
OPEN_EMPTY
TOPSPACE_EUCLIDEAN_SUBTOPOLOGY
CLOSED_UNION
OPEN_INTERS
BALL_TRIVIAL
BALL_MAX_UNION
BALL_SCALING
OPEN_CONTAINS_BALL_EQ
INTER_ACI_conjunct1
OPEN_SUBSET
OPEN_IN_TRANS
CLOSED_IN_TRANSLATION_EQ
CONNECTED_CLOSED_IN_EQ
CONNECTED_UNIONS
LIMPT_SUBSET
CLOSED_LIMPT
DISCRETE_IMP_CLOSED
INTERIOR_INTERIOR
OPEN_SUBSET_INTERIOR
INTERIOR_CLOSURE
CLOSURE_SUBSET
CLOSURE_MINIMAL_EQ
OPEN_INTER_CLOSURE_SUBSET
INTERIOR_DIFF
FRONTIER_UNIV
CONNECTED_INTER_FRONTIER
WITHIN_WITHIN
EVENTUALLY_HAPPENS
ALWAYS_EVENTUALLY
EVENTUALLY_FORALL
LIM_AT_INFINITY
LIM_WITHIN_OPEN
LIM_NEG
LIM_MIN
LIM_NULL_VMUL_BOUNDED
LIM_CONST_EQ
NETLIMIT_AT
LIM_TRANSFORM_WITHIN_SET
LIM_CASES_SEQUENTIALLY
CLOSED_APPROACHABLE
IN_INTERIOR_CBALL
CBALL_EQ_EMPTY
BOUNDED_SUBSET
FINITE_IMP_BOUNDED
BOUNDED_DIFF
BOUNDED_LINEAR_IMAGE
BOUNDED_DIFFS
BOUNDED_LIFT
CONVERGENT_BOUNDED_INCREASING
CONVERGENT_IMP_CAUCHY
CONVERGENT_IMP_BOUNDED
SEQUENCE_INFINITE_LEMMA
COMPACT_IMP_BOUNDED
COMPACT_EMPTY
FINITE_IMP_CLOSED
COMPACT_CBALL
COMPACT_DIFF
COMPACT_CHAIN
CONTINUOUS_AT
continuous_at
CONTINUOUS_ON_EQ_CONTINUOUS_AT
CONTINUOUS_ON_SING
LIM_CONTINUOUS_FUNCTION
CONTINUOUS_ABS
CONTINUOUS_ON_NEG
UNIFORMLY_CONTINUOUS_ON_CONST
CONTINUOUS_WITHIN_ID
UNIFORMLY_CONTINUOUS_ON_COMPOSE
CONTINUOUS_CLOSED_PREIMAGE
CONTINUOUS_AT_LIFT_DOT
CLOSED_STANDARD_HYPERPLANE
OPEN_HALFSPACE_COMPONENT_GT
CLOSURE_HALFSPACE_COMPONENT_GT
BOUNDED_HALFSPACE_LE
CONTINUOUS_CONSTANT_ON_CLOSURE
UNIFORMLY_CONTINUOUS_ON_CLOSURE
CAUCHY_CONTINUOUS_EXTENDS_TO_CLOSURE
BILINEAR_CONTINUOUS_ON_COMPOSE
CONTINUOUS_WITHIN_AVOID
OPEN_SCALING
COMPACT_CONTINUOUS_IMAGE
CONNECTED_LINEAR_IMAGE
CONNECTED_COMPONENT_TRANS
CONNECTED_COMPONENT_EQ_SELF
CONNECTED_COMPONENT_EQ
CONNECTED_COMPONENT_EQ_EQ
UNIONS_CONNECTED_COMPONENT
IN_COMPONENTS_NONEMPTY
COMPACT_UNIFORMLY_EQUICONTINUOUS
CONTINUOUS_ON_LIFT_RANGE
CONTINUOUS_ON_LIFT_COMPONENT
DISTANCE_ATTAINS_SUP
CONTINUOUS_ON_VMUL
CONTINUOUS_ON_INV
COMPACT_SUMS
DIAMETER_BOUNDED_BOUND
DIAMETER_SUBSET
COMPACT_CLOSED_SUMS
COMPLETE_TRANSLATION_EQ
interval_conjunct1
SUBSET_INTERVAL_IMP_conjunct2
SUBSET_INTERVAL_conjunct0
ENDS_IN_INTERVAL_conjunct1
CLOSED_INTERVAL
OPEN_INTERVAL_MIDPOINT
BOUNDED_SUBSET_CLOSED_INTERVAL
REAL_MIN_ACI_conjunct3
REAL_MAX_ACI_conjunct1
OPEN_CONTAINS_INTERVAL
CLOSED_OPEN_INTERVAL_1
IS_INTERVAL_INTERVAL
IS_INTERVAL_1_CASES
IN_SEGMENT
SEGMENT_1_conjunct0
IN_OPEN_SEGMENT
DIST_IN_CLOSED_SEGMENT
LIM_DROP_UBOUND
CONTINUOUS_ON_CASES
LIM_COMPONENTWISE_LIFT
HOMEOMORPHIC_REFL
HOMEOMORPHIC_INJECTIVE_LINEAR_IMAGE_LEFT_EQ
HOMEOMORPHIC_COMPACT
HOMEOMORPHIC_OPEN_INTERVAL_UNIV_1
OPEN_SURJECTIVE_LINEAR_IMAGE
LINEAR_IMAGE_SUBSET_INTERIOR
LIMPT_TRANSLATION_EQ
CLOSED_SUBSPACE
BASIS_COORDINATES_CONTINUOUS
VECTOR_EQ_AFFINITY
EXISTS_IN_GSPEC_conjunct0
RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS
IN_FROM
SERIES_0
SUMS_EQ
SUMS_REINDEX
SUMMABLE_RESTRICT
SEQUENCE_CAUCHY_WLOG
SUMMABLE_EQ_EVENTUALLY
SUMMABLE_IMP_TOZERO
SERIES_RATIO
SERIES_REARRANGE_EQ
CLOSEST_POINT_SELF
SEGMENT_TO_POINT_EXISTS
REAL_LE_SETDIST_EQ
CONTINUOUS_ON_LIFT_SETDIST
SETDIST_EQ_0_CLOSED_COMPACT
SEPARATION_NORMAL
SEGMENT_SYM_conjunct1
TIETZE_OPEN_INTERVAL_1
CLOSURE_DYADIC_RATIONALS
OPEN_SET_RATIONAL_COORDINATES
SUBSEQUENCE_DIAGONALIZATION_LEMMA
AFFINE_ALT
AFFINE_EMPTY
AFFINE_AFFINE_HULL
IN_AFFINE_ADD_MUL_DIFF
AFFINE_HULL_EXPLICIT
AFFINE_HULL_FINITE_STEP_conjunct1
AFFINE_HULL_INSERT_SPAN
CONVEX_EMPTY
CONVEX_HALFSPACE_LE
CONVEX_HALFSPACE_GT
CONVEX_INDEXED
CONIC_LINEAR_IMAGE_EQ
CONVEX_CONIC_HULL
AFFINE_DEPENDENT_EXPLICIT_FINITE
AFFINE_INDEPENDENT_2
COPLANAR_EMPTY
COPLANAR_LINEAR_IMAGE
CONVEX_CONNECTED
FRONTIER_NOT_EMPTY
CONNECTED_NEST
CONVEX_DISTANCE
SURA_BURA_COMPACT
CONVEX_TRANSLATION_EQ
CONVEX_HULL_UNIV
CONVEX_HULL_EQ_SING
CONVEX_HULL_UNION_NONEMPTY_EXPLICIT
CONVEX_HULL_3
AFFINE_HULL_SUBSET_SPAN
CLOSED_AFFINE
AFFINE_DEPENDENT_BIGGERSET
EMPTY_INTERIOR_AFFINE_HULL
AFFINE_PARALLEL_SLICE
AFF_DIM_AFFINE_HULL
AFF_DIM_LINEAR_IMAGE_LE
AFF_DIM_SUBSET
AFF_DIM_UNIV
AFFINE_INDEPENDENT_IFF_CARD
AFFINE_BOUNDED_EQ_TRIVIAL
AFFINE_HULL_INTER
CONVEX_HULL_EXCHANGE_INTER
AFF_DIM_AFFINE_INTER_HYPERPLANE
DIST_INCREASES_ONLINE
CLOSER_POINT_LEMMA
CONTINUOUS_AT_CLOSEST_POINT
SEPARATING_HYPERPLANE_CLOSED_POINT_INSET
SEPARATING_HYPERPLANE_SET_0_INSPAN
CONVEX_HULL_SCALING
HELLY
IS_INTERVAL_CONVEX_1
HOMEOMORPHIC_CLOSED_INTERVALS
CONVEX_CONE_CONTAINS_0
CONVEX_CONE_HULL_ADD
CONVEX_CONE_HULL_SEPARATE_NONEMPTY
CONVEX_CONE_NEGATIONS
FORALL_OF_DROP
CONVEX_ON_CONVEX_HULL_BOUND
CONVEX_ON_RIGHT_SECANT_MUL
SEGMENT_CONVEX_HULL
STARLIKE_TRANSLATION_EQ
RELATIVE_INTERIOR
RELATIVE_INTERIOR_SUBSET
RELATIVE_INTERIOR_INJECTIVE_LINEAR_IMAGE
INTERIOR_SUBSET_RELATIVE_INTERIOR
RELATIVE_INTERIOR_PROLONG
CONVEX_CLOSURE_RELATIVE_INTERIOR
CLOSURE_INTERS_CONVEX
SUPPORTING_HYPERPLANE_RELATIVE_BOUNDARY
INTERIOR_CONVEX_HULL_3_MINIMAL
SIMPLEX_EXPLICIT
PATHSTART_LINEAR_IMAGE_EQ
REVERSEPATH_LINEAR_IMAGE
ARC_LINEAR_IMAGE_EQ
ARC_DISTINCT_ENDS
CONNECTED_PATH_IMAGE
PATHFINISH_COMPOSE
PATHFINISH_REVERSEPATH
PATH_JOIN_IMP
ARC_JOIN
PATH_JOIN_PATH_ENDS
SHIFTPATH_TRANSLATION
PATH_IMAGE_SHIFTPATH
PATHSTART_SUBPATH
SUBPATH_LINEAR_IMAGE
SUBPATH_TO_FRONTIER_EXPLICIT
PATHSTART_LINEPATH
REVERSEPATH_LINEPATH
SUBPATH_REFL
PATH_COMPONENT_TRANS
PATH_CONNECTED_IFF_PATH_COMPONENT
PATH_COMPONENT_PATH_IMAGE_PATHSTART
OPEN_NON_GENERAL_COMPONENT
PATH_CONNECTED_CONTINUOUS_IMAGE
PATH_CONNECTED_UNION
CLOSURE_SEGMENT_conjunct1
CONVEX_SEGMENT_conjunct0
FINITE_SEGMENT_conjunct0
SUBSET_SEGMENT_conjunct1
INTER_SEGMENT
CARD_EQ_SEGMENT_conjunct1
HOMEOMORPHIC_MONOTONE_IMAGE_INTERVAL
PATH_COMPONENT_SUBSET_CONNECTED_COMPONENT
PATH_CONNECTED_OPEN_DELETE
IN_IMAGE_LIFT_DROP_conjunct1
PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX
OUTSIDE_TRANSLATION
INSIDE_INTER_OUTSIDE
UNBOUNDED_OUTSIDE
INTERIOR_INSIDE_FRONTIER
INSIDE_CONVEX
CLOSURE_INSIDE_SUBSET
INSIDE_INSIDE
HOMOTOPIC_WITH_EQ
HOMOTOPIC_COMPOSE_CONTINUOUS_RIGHT
HOMOTOPIC_PATHS_IMP_PATHSTART
HOMOTOPIC_PATHS_TRANS
HOMOTOPIC_PATHS_JOIN
HOMOTOPIC_PATHS_LINV
HOMOTOPIC_LOOPS_TRANS
PATH_CONNECTED_EQ_HOMOTOPIC_POINTS
HOMOTOPIC_PATHS_LOOP_PARTS
SIMPLY_CONNECTED_EQ_CONTRACTIBLE_PATH
HOMEOMORPHIC_CONTRACTIBLE
STARLIKE_IMP_CONTRACTIBLE
FACE_OF_TRANSLATION_EQ
FACE_OF_TRANS
FACE_OF_STILLCONVEX
FACE_OF_IMP_CONVEX
FACE_OF_DISJOINT_INTERIOR
EMPTY_EXPOSED_FACE_OF
EXPOSED_FACE_OF_INTERS
EXTREME_POINT_NOT_IN_RELATIVE_INTERIOR
EXTREME_POINT_OF_LINEAR_IMAGE
EXTREME_POINT_OF_CONVEX_HULL_INSERT
FACET_OF_LINEAR_IMAGE
KREIN_MILMAN
EXTREME_POINT_OF_CONVEX_HULL_2
SEGMENT_FACE_OF
FACE_OF_POLYTOPE_POLYTOPE
POLYTOPE_IMP_CLOSED
POLYHEDRON_POSITIVE_ORTHANT
AFFINE_IMP_POLYHEDRON
POLYHEDRON_INTER_AFFINE_PARALLEL_MINIMAL
FACET_OF_POLYHEDRON
FINITE_POLYHEDRON_EXPOSED_FACES
POLYHEDRON_EQ_FINITE_FACES
POLYTOPE_FACET_EXISTS
POLYHEDRON_AS_CONE_PLUS_CONV
FRONTIER_OF_TRIANGLE
AFF_DIM_SIMPLEX
HAS_SIZE_FACES_OF_SIMPLEX
BINOM_BOTTOM_STEP
BROUWER_COMPACTNESS_LEMMA
IMAGE_LEMMA_1
POINTWISE_MAXIMAL
KLE_MAXIMAL
KLE_SUC
KSIMPLEX_EXTREMA_STRONG
KSIMPLEX_FIX_PLANE_P
REDUCED_LABELLING_UNIQUE
KSIMPLEX_0
RETRACT_OF_SUBSET
RETRACT_OF_REFL
ABSOLUTE_RETRACT_PATH_IMAGE_ARC
BROUWER_BALL
CONTINUOUS_ON_INTERVAL_BIJ
FASHODA_UNIT
HOMEOMORPHIC_EMPTY_conjunct0
HAS_DERIVATIVE_WITHIN
HAS_DERIVATIVE_CONST
HAS_DERIVATIVE_VSUM
HAS_DERIVATIVE_TRANSFORM_WITHIN_OPEN
JACOBIAN_WORKS
DIFFERENTIABLE_WITHIN_SUBSET
DIFFERENTIABLE_CONST
DIFFERENTIABLE_CHAIN_AT
FRECHET_DERIVATIVE_AT
DIFFERENTIAL_ZERO_MAXMIN
DIFFERENTIABLE_BOUND
HAS_DERIVATIVE_INVERSE_BASIC_X
HAS_DERIVATIVE_LOCALLY_INJECTIVE
HAS_DERIVATIVE_BILINEAR_AT
HAS_VECTOR_DERIVATIVE_CONST
CONVEX_ON_DERIVATIVES_IMP
INTERVAL_UPPERBOUND
CONTENT_UNIT
CONTENT_0_SUBSET
CONTENT_SUBSET
GAUGE_BALL
DIVISION_OF_FINITE
FORALL_IN_DIVISION
ELEMENTARY_INTER
ELEMENTARY_SUBSET_INTERVAL
DIVISION_OF_NONTRIVIAL
TAGGED_PARTIAL_DIVISION_SUBSET
TAGGED_PARTIAL_DIVISION_OF_TRIVIAL
TAGGED_PARTIAL_DIVISION_OF_SUBSET
has_integral
INTERVAL_BISECTION_STEP
INTEGRAL_EQ_HAS_INTEGRAL
HAS_INTEGRAL_NEG
INTEGRAL_NEG
INTEGRABLE_SUB
HAS_INTEGRAL_EQ
HAS_INTEGRAL_EMPTY
INTERVAL_SPLIT
DIVISION_SPLIT
PROPERTY_EMPTY_INTERVAL
OPERATIVE_INTEGRAL
ADDITIVE_CONTENT_TAGGED_DIVISION
DSUM_BOUND
INTEGRAL_COMPONENT_LE
HAS_INTEGRAL_COMPONENT_NEG
DROP_INDICATOR_LE_1
TAGGED_DIVISION_FINER
NEGLIGIBLE_SUBSET
NEGLIGIBLE_INSERT
INTEGRAL_EQ
MONOIDAL_AND
OPERATIVE_1_LT
INTEGRABLE_SUBINTERVAL
HAS_INTEGRAL_TWIDDLE
HAS_INTEGRAL_REFLECT_LEMMA
FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG
HAS_INTEGRAL
INTEGRAL_RESTRICT_INTER
INTEGRAL_SPIKE_SET
HAS_INTEGRAL_ALT
POWERSET_CLAUSES_conjunct1
INTEGRABLE_STRADDLE
HAS_INTEGRAL_COMBINE_DIVISION
HAS_INTEGRAL_COMBINE_TAGGED_DIVISION
MONOTONE_CONVERGENCE_INCREASING
HAS_BOUNDED_SETVARIATION_ON_ELEMENTARY
HAS_BOUNDED_SETVARIATION_ON_CMUL
SET_VARIATION_ON_ELEMENTARY
SET_VARIATION_UBOUND_ON_INTERVAL
SET_VARIATION_ON_NULL
ABSOLUTELY_INTEGRABLE_LE
ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION
ABSOLUTELY_INTEGRABLE_ADD
ABSOLUTELY_INTEGRABLE_MAX_1
ABSOLUTELY_INTEGRABLE_INTEGRABLE_BOUND
ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_UBOUND
DOMINATED_CONVERGENCE
BEPPO_LEVI_DECREASING
EQUIINTEGRABLE_LIMIT
EQUIINTEGRABLE_SUB
EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE
INDEFINITE_INTEGRAL_CONTINUOUS_LEFT
INTEGRABLE_INCREASING_PRODUCT
INTEGRABLE_DECREASING
HAS_BOUNDED_VARIATION_ON_SUB
HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS
VECTOR_VARIATION_MONOTONE
VECTOR_VARIATION_ON_DIVISION
HAS_BOUNDED_VARIATION_DARBOUX
HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT
INTEGRAL_PASTECART_CONTINUOUS
MEASURABLE
HAS_MEASURE_INTERVAL_conjunct1
MEASURE_INTERVAL_2_conjunct0
MEASURE_DISJOINT_UNION
HAS_MEASURE_0
MEASURABLE_MEASURE_POS_LT
HAS_MEASURE_DIFF_NEGLIGIBLE
MEASURE_NEGLIGIBLE_UNION_EQ
MEASURE_NEGLIGIBLE_UNIONS
HAS_MEASURE_NEGLIGIBLE_UNIONS_IMAGE_STRONG
MEASURE_UNIONS_LE_IMAGE
HAS_MEASURE_LIMIT
HAS_MEASURE_AFFINITY
NEGLIGIBLE_TRANSLATION_REV
MEASURE_SCALING
MEASURABLE_INTERVAL_conjunct0
MEASURABLE_COUNTABLE_UNIONS
MEASURABLE_COMPACT
MEASURE_INTERIOR
STARLIKE_NEGLIGIBLE_BOUNDED_MEASURABLE
NEGLIGIBLE_AFFINE_HULL
NEGLIGIBLE_SPHERE
NEGLIGIBLE_LINEAR_SINGULAR_IMAGE
MEASURABLE_OUTER_CLOSED_INTERVALS
INDUCT_MATRIX_ROW_OPERATIONS
HAS_MEASURE_SHEAR_INTERVAL
NEGLIGIBLE_LINEAR_IMAGE
HAS_MEASURE_IMAGE_STD_SIMPLEX
HAS_MEASURE_TETRAHEDRON
INTEGRABLE_CCONTINUOUS_EXPLICIT_SYMMETRIC
INTEGRABLE_SUBINTERVALS_IMP_MEASURABLE
MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET
MEASURABLE_ON_NEG
MEASURABLE_ON_SUB
MEASURABLE_ON_COMPONENTWISE
NEGLIGIBLE_LOCALLY_LIPSCHITZ_IMAGE
LEBESGUE_MEASURABLE_UNION
LEBESGUE_MEASURABLE_OPEN
CONTINUOUS_IMP_MEASURABLE_ON_CLOSED_SUBSET
MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE
MEASURABLE_ON_PREIMAGE_CLOSED_INTERVAL
MEASURABLE_MEASURABLE_DIFF_LEGESGUE_MEASURABLE
ITER_ADD
COMPLEX
complex_norm
COMPLEX_MUL_SYM
COMPLEX_ADD_RINV
COMPLEX_MUL_RNEG
COMPLEX_NEG_SUB
COMPLEX_EQ_SUB_RADD
COMPLEX_ENTIRE
CX_SUB
COMPLEX_NORM_CX
IM_NEG
IM_II
RE_MUL_CX
COMPLEX_INV_0
COMPLEX_MUL_AC_conjunct1
COMPLEX_INV_EQ_0
COMPLEX_POW_2
COMPLEX_POW_ZERO
COMPLEX_NORM_MUL
CNJ_CX
CNJ_MUL
CNJ_EQ_0
RE_COMPLEX_DIV_EQ_0
IM_COMPLEX_INV_GE_0
CX_SQRT
POW_2_CSQRT
VSUM_COMPLEX_LMUL
COMPLEX_SUB_POW_R1
REAL_MUL_CX
REAL_VSUM
REAL_NORM
VSUM_GP
COMPLEX_POLYFUN_ROOTBOUND
CPRODUCT_MUL
OPEN_HALFSPACE_RE_LT
CLOSED_REAL_SET
LIM_COMPLEX_DIV
SERIES_COMPLEX_RMUL
CONTINUOUS_COMPLEX_POW
LIM_CONTINUOUS
LINEAR_CX_IM
HAS_COMPLEX_DERIVATIVE_IMP_CONTINUOUS_WITHIN
COMPLEX_DIFFERENTIABLE_AT_WITHIN
COMPLEX_DIFF_CHAIN_WITHIN
HAS_COMPLEX_DERIVATIVE_AT
HAS_COMPLEX_DERIVATIVE_RMUL_AT
HAS_COMPLEX_DERIVATIVE_ADD
HAS_COMPLEX_DERIVATIVE_INV_BASIC
COMPLEX_DIFFERENTIABLE_LINEAR
COMPLEX_DIFFERENTIABLE_INV_WITHIN
COMPLEX_DIFFERENTIABLE_COMPOSE_WITHIN
HOLOMORPHIC_ON_ADD
HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE
COMPLEX_DERIVATIVE_LMUL
ANALYTIC_ON_HOLOMORPHIC
ANALYTIC_ON_INV
HAS_COMPLEX_DERIVATIVE_INVERSE_BASIC
COMPLEX_DERIVATIVE_JACOBIAN
REAL_LIM
SUMS_GP
SUM_INTEGRAL_UBOUND_INCREASING
ABEL_POWER_SERIES_CONTINUOUS
CEXP_CONVERGES_UNIFORMLY
CEXP_NEG_RMUL
CEXP_N
CSIN_CIRCLE
CCOS_DOUBLE
COMPLEX_MUL_CCOS_CCOS
CNJ_CEXP
REAL_EXP_SUB
REAL_EXP_MONO_IMP
CNJ_CSIN
HAS_COMPLEX_DERIVATIVE_CSIN
CONTINUOUS_AT_CCOS
COS_DOUBLE_COS
SIN_SUB
IM_CEXP
IVT_DECREASING_RE
LOG_1
LOG_POW
COS_NONTRIVIAL
SIN_HASZERO_MINIMAL
COS_PI
COS_NPI
SIN_EQ_0
SIN_COS_SQRT
CIRCLE_SINCOS
CEXP_COMPLEX
CEXP_EQ
TAYLOR_CSIN
ARG_DIV_CX
ARG_EQ_PI
ARG_LE_DIV_SUM_EQ
ROTATE2D_0
ROTATE2D_ADD
COMPLEX_DIV_ROTATION
CTAN_NEG
COMPLEX_DIFFERENTIABLE_AT_CTAN
TAN_NEG
TAN_POS_PI2
SIN_MONO_LT_EQ
COS_MONO_LE_EQ
SIN_PI6_STRADDLE
COMPLEX_DIFFERENTIABLE_AT_CLOG
IM_CLOG_POS_LE
CLOG_1
COMPLEX_DIFFERENTIABLE_AT_CSQRT
CPOW_ADD
CLOG_MUL_SIMPLE
RE_CATN_BOUNDS
TAN_ATN
ATN_POS_LE
SIN_ATN
CASN_BODY_LEMMA
HAS_COMPLEX_DERIVATIVE_CASN
CACS_UNIQUE
CONTINUOUS_AT_CACS
CACS_BOUNDS
CX_ASN
ASN_NEG_1
REAL_ACS
ACS_1
ACS_MONO_LT
ASN_ACS
CONTINUOUS_WITHIN_CACS_REAL
LIM_1_OVER_LOG
FINITE_COMPLEX_ROOTS_UNITY
CONTINUOUS_WITHIN_UPPERHALF_ARG
ROOT_WORKS
REAL_ROOT_MUL
ROOT_EXP_LOG
RPOW_LE2
RPOW_INV
REAL_OPEN_UNIV
REAL_CLOSED_EMPTY
REAL_CLOSED_HALFSPACE_LE
REAL_BOUNDED_POS_LT
REALLIM_COMPLEX
REALLIM_RMUL_EQ
REALLIM_INV
REALLIM_NULL
REAL_SEQ_OFFSET
REALLIM_AT
REAL_SUMS
REAL_SUMS_INFSUM
REAL_SUMMABLE_IFF_COFINITE
REAL_SERIES_RMUL
REAL_INFSUM
REAL_SERIES_COMPARISON
TRIVIAL_LIMIT_AT_POSINFINITY
EVENTUALLY_ATREAL
LIM_AT_NEGINFINITY
LIM_WITHINREAL_SUBSET
LIM_ATREAL_AT
REAL_CONTINUOUS_WITHIN
real_continuous_within
REAL_CONTINUOUS_WITHINREAL_SUBSET
REAL_CONTINUOUS_LMUL
REAL_CONTINUOUS_INV
REAL_CONTINUOUS_INV_WITHIN
REAL_CONTINUOUS_ATREAL_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_ATREAL_COMPOSE
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN
REAL_CONTINUOUS_ON_LMUL
REAL_CONTINUOUS_ON_POW
REAL_CONTINUOUS_ATTAINS_INF
CONTINUOUS_COMPONENTWISE
HAS_REAL_FRECHET_DERIVATIVE_WITHIN
REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE
IS_REALINTERVAL_IS_INTERVAL
IMAGE_LIFT_DROP_conjunct0
INTERVAL_REAL_INTERVAL_conjunct1
REAL_OPEN_CLOSED_INTERVAL
REAL_COMPACT_INTERVAL
REAL_CONTINUOUS_CONTINUOUS_ATREAL
HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL
REAL_CONTINUOUS_AT_ARG
HAS_REAL_DERIVATIVE_TRANSFORM_ATREAL
REAL_DERIVATIVE_UNIQUE_ATREAL
HAS_REAL_DERIVATIVE_ID
HAS_REAL_DERIVATIVE_MUL_ATREAL
HAS_REAL_DERIVATIVE_DIV_WITHIN
REAL_DIFFERENTIABLE_ADD
REAL_DIFFERENTIABLE_TRANSFORM_WITHIN
REAL_DIFFERENTIABLE_ON_ADD
REAL_CONTINUOUS_WITHIN_EXP
REAL_DIFFERENTIABLE_AT_COS
REAL_CONTINUOUS_WITHIN_TAN
REAL_DIFFERENTIABLE_AT_SQRT
HAS_REAL_DERIVATIVE_ASN_COS
REAL_DIFFERENTIABLE_AT_ACS
REAL_CONTINUOUS_WITHIN_ACS_STRONG
REAL_IVT_INCREASING
ENDS_IN_REAL_INTERVAL_conjunct1
REAL_MVT
HAS_REAL_DERIVATIVE_SEQUENCE
REAL_SUM_INTEGRAL_LBOUND_INCREASING
REAL_SEGMENT_SEGMENT_conjunct0
REAL_CONVEX_ON_SECANT_DERIVATIVE
HAS_REAL_INTEGRAL
HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL
HAS_REAL_INTEGRAL_LINEAR
REAL_INTEGRAL_0
REAL_INTEGRABLE_SUB
REAL_INTEGRABLE_EQ
HAS_REAL_INTEGRAL_LE
HAS_REAL_INTEGRAL_SPIKE
REAL_NEGLIGIBLE_EMPTY
REAL_INTEGRAL_EQ
HAS_REAL_INTEGRAL_AFFINITY
HAS_REAL_INTEGRAL_RESTRICT
HAS_REAL_INTEGRAL_OPEN_INTERVAL
REAL_INTEGRABLE_STRADDLE
ABSOLUTELY_REAL_INTEGRABLE_LMUL
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE
HAS_REAL_MEASURE
REAL_MEASURE_MEASURE
REAL_MEASURE_DISJOINT_UNION
REAL_MEASURE_EQ_0
REAL_MEASURABLE_DIFF
HAS_REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS_IMAGE
REAL_MEASURE_UNIONS_LE_IMAGE
HAS_REAL_MEASURE_TRANSLATION_EQ
REAL_MEASURABLE_COUNTABLE_UNIONS_STRONG
IN_IMAGE_DROPOUT
DOT_PUSHIN
SLICE_INTERVAL
SLICE_INTER
SLICE_BALL
FUBINI_SIMPLE_ALT
REAL_OPEN_SET_EXISTS_RATIONAL
REAL_CONTINUOUS_FLOOR
UNCOUNTABLE_CONTAINS_LIMIT_POINT
STONE_WEIERSTRASS
CONTINUOUS_ON_VECTOR_POLYNOMIAL_FUNCTION
MEASURABLE_ON_COMPLEX_DIV
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS
REAL_MEASURABLE_ON_ADD
REAL_LEBESGUE_MEASURABLE_EMPTY
REAL_LEBESGUE_MEASURABLE_COMPL
REAL_MEASURABLE_ON_LEBESGUE_MEASURABLE_SUBSET
REAL_SECOND_MEAN_VALUE_THEOREM_BONNET_FULL
ABSOLUTELY_REAL_INTEGRABLE_DECREASING_PRODUCT
REAL_VARIATION_MONOTONE
VECTOR_ANGLE_LINEAR_IMAGE_EQ
VECTOR_ANGLE_RNEG
VECTOR_ANGLE_EQ_PI
SIN_VECTOR_ANGLE_EQ
VECTOR_ANGLE_EQ
VECTOR_ANGLE_EQ_0_LEFT
SIN_SQUARED_VECTOR_ANGLE
ANGLE_EQ_PI_DIST
ANGLE_RANGE
COLLINEAR_SIN_ANGLE_IMP
LAW_OF_SINES
CONGRUENT_TRIANGLES_SSS
ANGLE_BETWEEN
CROSS_RZERO
CROSS_RMUL
Trigonometry1.BASIS_3_conjunct0
CROSS_EQ_0
CROSS_LINEAR_IMAGE_WEAK
COLLINEAR_SPECIAL_SCALE
SLICE_DROPOUT_3
Counting_spheres.pad2d3d_dot_v
COPLANAR
AFFSIGN_INJECTIVE_LINEAR_IMAGE
AFFSIGN_TRANSLATION
AFF_GT_3_1
AFFSIGN_SUBSET_AFFINE_HULL
AFFSIGN_SUBSET_AFFSIGN
AFFSIGN_MONO_RIGHT
AFF_GE_SPECIAL_SCALE
AFF_GE_0_CONVEX_CONE_NEGATIONS
SEGMENT_SUBSET_HALFLINE
CONV0_AFF_GT
MEASURE_CONV0_CONVEX_HULL
ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT
AZIM_UNIQUE
Trigonometry2.LT_IMP_ABS_REFL
CROSS_BASIS_conjunct0
AZIM_EQ_ALT
AZIM_EQ_PI_SYM
DIHV
AZIM_DIHV_SAME
DIHV_EQ_0_PI_EQ_COPLANAR
WEDGE_TRANSLATION
WEDGE_LUNE
OPEN_WEDGE
VOLUME_CBALL
BOUNDED_CONIC_CAP
NEGLIGIBLE_RCONE_EQ
HAS_MEASURE_OPEN_SECTOR_LT_GEN
AFF_GT_SHUFFLE
MEASURABLE_BOUNDED_INTER_OPEN
VOLUME_CONIC_CAP_COMPL
MEASURABLE_RULES_conjunct2
VERTICES_LINEAR_IMAGE
Sphere.dihV
Geomdetail.v3_in_convex3
Geomdetail.simpl_conv3
Geomdetail.VSUM_DIS2
Geomdetail.CONV3_A_EQ
Geomdetail.CARD2
Geomdetail.HAS_SIZE_SET_OF_LIST_4
Geomdetail.U_IN_CONV2
Geomdetail.PAIR_EQ_EXPAND
Collect_geom.lemma7
Collect_geom.VSUM_DIS2
Collect_geom.IN_SET3
Collect_geom.LEFT_END_POINT
Collect_geom.ETA_X_SYM
Collect_geom.RE_TRUONGG
Collect_geom.IN_CONV_COLLINEAR
Collect_geom.TRIVIVAL_LE
Collect_geom.LAMBDA_TRIPLED_THM
Collect_geom.simp_def2_conjunct1
Collect_geom.AFFINE_SET_GEN_BY_TWO_POINTS
Collect_geom.AFFINE_CONTAIN_LINE
Collect_geom.D3_POS_LE
Collect_geom.X_DOT_X_EQ
Collect_geom.SDIHJZK_INTERPRETE
Collect_geom.DELTA_X1I_RRR_conjunct2
Collect_geom.NEVER_USED_AGAIN
Collect_geom.NOT_COLL_IMP_RADV_EQ_ETA_Y
Collect_geom.MUL3_SYM
Collect_geom.LEMMA50
Collect_geom.NONCOPLANAR_3_BASIS
Collect_geom.DISCRIMINANT_OF_CAY
Collect_geom2.PRE_VIET
Collect_geom2.SUB_DOT_NEG_TO_POS
Collect_geom2.FACTOR_OF_QUADRARTIC
Collect_geom2.REAL_LE_RDIV_0
Collect_geom2.GREATER_THAN_MID_QUADRATIC_PO
Collect_geom2.CONVEX_HULL4
Collect_geom2.AFF_GT33
Collect_geom2.AFF_GES_GTS
Collect_geom2.ALL_ABOUT_COEF_2
Collect_geom2.BPOW8APOW2CPOW2
Collect_geom2.VEC3_EQ_EX
Collect_geom2.IN_PLANE_IMP_OTHORGONAL
Collect_geom2.SUM_CHI_EQ_2DELTA
FORALL_IN_CLAUSES_conjunct1
Collect_geom2.PROVE_IN_AFFINE_HULL_4
Collect_geom2.NOT_COL_EQ_UPS_X_POS
Collect_geom2.LLEEMAA
Collect_geom2.NOT_COPLANAR_IMP_NOT_COLLINEAR
Real_ext.REAL_MUL_RTIMES_LE
Tactics_jordan.strict_lemma
Num_ext_nabs.INT_IS_INT
Taylor_atn.pos1
Taylor_atn.atn_half_range
Taylor_atn.atn_half
Taylor_atn.id4a
Taylor_atn.taylor_series_inv_pow
Taylor_atn.term_bound
Taylor_atn.real_taylor_atn_halfatn4
Float.TWOPOW_NEG
Float.TWOPOW_ADD_INT
Float.FLOAT_ADD_PN
Float.INT_ABS_NEG_NUM
Float.FLOAT_LT
Float.INTERVAL_SUB
Float.INTERVAL_MAX
Float.taylor_atn
Float.REAL_SSQRT_MONO
Float.FLOAT_ZERO
Float.INTERVAL_TO_LESS
Flyspeck_constants.bounds_conjunct10
Flyspeck_constants.bounds_conjunct16
Misc_defs_and_lemmas.ABS_SQUARE
Misc_defs_and_lemmas.sub_union
Misc_defs_and_lemmas.GSPEC_THM
Misc_defs_and_lemmas.num_SEG_UNION
Misc_defs_and_lemmas.INVERSE_BIJ
Misc_defs_and_lemmas.DOMAIN_EMPTY
Trigonometry1.SIN_PERIODIC_N2PI
Trigonometry1.ATAN2_EXISTS
Trigonometry1.ATN2_0_NEG_1
Trigonometry1.ATN2_ARCLENGTH
Trigonometry.HQTBPCM2
Trigonometry1.COMPONENTS_3
Trigonometry.UKBAHKV
Trigonometry2.ABS_LE_1_IMP_SIN_ACS
Trigonometry2.MOVE_NORM_OUT_OF_SQRT
Trigonometry2.NOT_IDEN_IMP_ABS_LE
Trigonometry2.ARC_SYM
Trigonometry2.DIST_TRANSABLE
Trigonometry2.NOT_ZERO_EQ_POW2_LT
Trigonometry2.AFFINE_SET_GENERARTED2
Trigonometry2.WHEN_K_POS_ARCV_STABLE
Trigonometry2.SIN_EQ_SQRT_ONE_SUB
Trigonometry2.ARCV_BOUNDED
Trigonometry.KEITDWB
DOT_CROSS_SELF_conjunct1
Trigonometry2.SUBSET_AFFINE_HULL3_EQ_SUB_PLANE
Trigonometry2.POW2_1_BOUNDED
Trigonometry2.PERIODIC_AT0_IMP_ANY
Trigonometry2.IN_ORIGIN_PERIOD_IMP_UNIQUENESS
Collect_geom.SUB_SUM_SUB_conjunct0
Trigonometry2.R_SIN_COS_IDENT
Trigonometry2.TWO_UNIT_ORTH_VECTORS_IMP_ORTHONORMAL
Trigonometry2.IMAGE_INTER_AFF3
Trigonometry2.ORTHOGORNAL_UNITIZE
Trigonometry2.INSERT_INTER_EMPTY_conjunct1
Trigonometry2.CART2_EQ
Trigonometry2.NORM_VECTOR2_TRIG
Trigonometry2.TOW_NON_VEC0_IMP_NOT_REFL_POLAR_LT
Trigonometry2.TDHUFHCYVHYBCC
Trigonometry2.MONO_LE_IN_FIRST_PERIOD
Trigonometry2.SUM_INCREASE_ARG_DIFF
Calc_derivative.ratform_add
Calc_derivative.trivial_ratform
Calc_derivative.imp_lt
Calc_derivative.derived_form_pow
Calc_derivative.derived_form_atn
Calc_derivative.x2notless0
Calc_derivative.derived_imp_pos_open_3
Calc_derivative.atn_lemma
Calc_derivative.atn2_atn_open_2
Calc_derivative.derived_form_atn2curry
Nonlinear_lemma.sqrt2_nn
Nonlinear_lemma.dih_x_y
Nonlinear_lemma.dih_y_sym
Nonlinear_lemma.rho_alt
Nonlinear_lemma.edge_flat2_x_rewrite
Nonlinear_lemma.h0_lt_hplus
Nonlinear_lemma.vol4f_lmfun
Nonlinear_lemma.lmdih0
Nonlinear_lemma.vol3_vol_x
Nonlinear_lemma.tame_table_d_values_conjunct0
Delta_x.COMPUTE_DELTA_X
Euler_complement.COMPUTE_DELTA_X_AFTER_RESCALE
Euler_multivariate.HAS_REAL_DERIVATIVE_ZERO_CONSTANT2
Hvihvec.VECTOR_ANGLE_DOUBLECROSS
Vol1.normball_ellip0
Vol1.rs_sr_unit
Vol1.normball_subset
Vol1.pre_def_4_3b
Vol1.inter_radial
Vol1.vector_eq1
Vol1.disjoint_line_interval
Vol1.measurable_cube
Vol1.negligible_cube
Vol1.measure_unions_cube_less_ball
Vol1.surj2_map1
Vol1.measure_ccube
Vol1.ccube_to_ball
Vol1.card_int_ball_ineq
Vol1.bdt2_finiteness
Vol1.bdt7_finiteness
Hypermap.edge_map_and_darts
Hypermap.orbit_subset
Hypermap.lemma_add_exponent_function
Hypermap.power_permutation
Hypermap.edge_map_inverse_representation
Hypermap.lemma_dart_invariant_power_node
Hypermap.LEMMA_INJ
Hypermap.LT1_NZ
Hypermap.LT_RIGHT_SUC
Hypermap.le_compare_right
Hypermap.lemma_inj_list
Hypermap.lemma_list_disjoint2
Hypermap.first_join_evaluation
Hypermap.lemma_permutation_via_its_inverse
Hypermap.orbit_sym
Hypermap.node_refl
Hypermap.FINITE_TWO_ELEMENTS
Hypermap.lemma_card_of_disjoint_covering
Hypermap.lemmaTGJISOK
Hypermap.lemma_face_subset
Hypermap.lemma_glue_paths
Hypermap.partition_components
Hypermap.lemma_face_contour
Hypermap.lemma_pair_representation
Hypermap.walkup_permutes
Hypermap.lemma_node_degenerate
Hypermap.edge_map_walkup
Hypermap.lemma_segment_orbit
Hypermap.lemma_edge_identity
Hypermap.lemma_inverse_in_orbit
Hypermap.lemma_orbit_eq
Hypermap.lemma_walkup_edges
Hypermap.lemma_edge_representation
Hypermap.lemma_edge_map_walkup_in_dart
Hypermap.lemma_edge_merge
Hypermap.lemma_face_subset_component
Hypermap.node_degenerate_walkup_node_map
Hypermap.edge_degenerate_walkup_third_eq
Hypermap.LEMMA_CARD_DIFF
Hypermap.NODE_NOT_EMPTY
Hypermap.lemma_in_components
Hypermap.lemma_card_walkup_dart
Hypermap.lemma_walkup_count_not_splitting_components
Hypermap.convolution_inv
Hypermap.lemma_orbit_of_size_2
Hypermap.CARD_UNION_EDGES_LE
Hypermap.power_permutation_outside_domain
Hypermap.lemma_representaion_Wn
Hypermap.lemma_first_dart_on_inj_contour
Hypermap.lemma_shift_contour
Hypermap.concatenate_two_contours
Hypermap.lemma_minimum_Moebius_hypermap
Hypermap.lemma_card_node_walkup_dart
Hypermap.lemma_node_walkup_eliminate_dart_on_Moebius_contour
Hypermap.lemma_transitive_permutation
Hypermap.lemma_permutes_via_surjetive
Hypermap.lemma_generate_loop
Hypermap.lemma_inj_face_contour
Hypermap.lemma_node_inverse_cycle
Hypermap.lemma_transitive_going
Hypermap.lemma_atom_sub_node
Hypermap.lemma_in_dart
Hypermap.disjoint_loops
Hypermap.node_map_on_margin
Hypermap.atom_one_point
Hypermap.I_BIJ
Hypermap.lemma_sub_support
Hypermap.lemma_in_QuotientNode
Hypermap.lemma_edge_nondegenerate
Hypermap.lemma_power_inverse_in_node2
Hypermap.lemma_increasing_index_one
Hypermap.lemma_inc_injective
Hypermap.lemma_inj_complement
Hypermap.lemma_marked_dart
Hypermap.atom_eq
RC_CLOSED
SC_MONO
TC_SYM
TC_CASES_R
RSC_CLOSED
RTC_INDUCT
STC_TRANS
RSTC_INC
SC_INV
Fan_defs.N_FAN_PAIR_EXT
Fan.fan6
Fan.FAN1_LINEAR_IMAGE_EQ
Fan.FAN5_LINEAR_IMAGE_EQ
Fan.properties_of_set_of_edge
Fan.th3b1
Fan.th4
Fan.SIGMA_FAN
Fan.UNIQUE1_POINT_FAN
Fan.property_of_cyclic_set
Fan.image_power_map_points
Fan.norm_of_normal_vector_is_unit_fan
Fan.e1_is_normal_fan
Fan.vdot_e2_fan
Fan.module_of_vector
Fan.sincos1_of_u_fan
Fan.MONO_SIGMA_FAN
Fan.SUR_N_FAN
Fan.condition_hypermap_fan
Fan.distinct_nodes
Fan.FACE_FAN_NOT_EMPTY
Fan.into_domain_n_fan
Fan.into_domain_power_efn_fan
Fan.face_subset_dart_fan
Topology.MONO_POWER_SIGMA_FAN
Topology.i_IN_ORBITS_FAN
Topology.ORBITS_SIGMA_FAN
Topology.ORBITS_EQ_SET_EDGE_FAN
Topology.SUM_AZIM_POWER_SIGMA_FAN
Topology.COMPLEMENT_SET_FAN
Topology.UNION_FAN
Topology.disjiont1_cor6dot1
Topology.closed_aff_ge_2_1
Topology.bounded_ballnorm_fan
Topology.exists_ballsets_fan
Topology.inter_is_empty
Topology.expand_edge_graph_fan
Topology.r3_ge_is_convex_fan
Topology.one_edge_fan
Topology.DART_LEADS_INTO
Fan_misc.EXTENSION_SIGMA_FAN_INJECTIVE
Planarity.open_vector_angle_fan
Planarity.separate_point_convex_fan
Planarity.bounded_convex_fan
Planarity.scale_aff_ge_fan
Planarity.injective_azim_coplanar
Planarity.fan_run_in_small3_is_fan
Planarity.not_collinear_is_properties_fully_surrounded1
Planarity.cross_dot_fully_surrounded_fan
Planarity.cross_dot_fully_surrounded2_fan
Planarity.aff_gt_subset_aff_ge
Planarity.aff_gt3_subset_aff_gt
Planarity.point_in_aff_ge
Planarity.AFFINE_HULL_1
Planarity.lemma_proof1_fan
Planarity.inequality1_not0_fan
Planarity.fan_run_in_small2_not0_is_fan
Planarity.lie_in_half_space_and_azim_le
Planarity.AFF_GT_CUT_XFAN_IMP_EDGE_FAN
Planarity.in_aff_2_2_fan
Planarity.exists_rw_dart_inter_aff_gt_fan
Planarity.aff_gt_1_2_scale_fan
Planarity.connected_component_of_faces_fan
Planarity.exists_point_dart_leads_into_fan
Planarity.condition_not_edge_fan
Planarity.exists_point_in_component_yfan
Planarity.aff_gt_connect_bound_subset_yfan
Planarity.sym_line_fan
Planarity.notempty_xfan_inter_segment_fan
Planarity.expand_element_in_topological_component_yfan
Planarity.place_there_point_line_fan
Planarity.no_origin_aff_ge_is_aff_gt
Planarity.exists_edge_bounded_topological_component_yfan
Planarity.exists_dart_leads_into_edge_eq_topological_component_fan
Planarity.aff_gt_1_2_cross_dotr_4point_neg
Planarity.point_in_aff_gt_2_1_change_point_in_aff_gt_1_2
Planarity.AFF_GT_1_3
Planarity.aff_gt_1_3_subset_yfan
Planarity.OPEN_DIFF_AFF_GE
Planarity.KVQWYDL_lemma1
Planarity.condition_unique_by_dart_leads_into
Planarity.KVQWYDL_lemma3
Planarity.CARD_FACE_SET_EQ_3_FULLY_SURROUNDED_FAN1
Planarity.ball_eq_normball
Hypermap_and_fan.IMAGE_LEMMA
Hypermap_and_fan.RES_PERMUTES
Hypermap_and_fan.F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN
Hypermap_and_fan.HYPERMAP_OF_FAN
Hypermap_and_fan.DART1_OF_FAN_SUBSET_DART_OF_FAN
Hypermap_and_fan.PAIR_IN_DART1_OF_FAN
Hypermap_and_fan.FINITE_ORBIT_MAP
Hypermap_and_fan.SUM_ORBIT
Hypermap_and_fan.LINEAR_FACE
Hypermap_and_fan.PLAIN_HYPERMAP_OF_FAN
Hypermap_and_fan.NODE_HYPERMAP_OF_FAN
Hypermap_and_fan.FST_NODE_lemma
Hypermap_and_fan.AZIM_I_FAN_EQ_AZIM_DART
Hypermap_and_fan.SURROUNDED_IMP_IN_DART1_OF_FAN
Hypermap_and_fan.HYPERMAP_OF_FAN_NO_LOOPS
Conforming.IMAGE_F1_IN_FACE_IMP_IN_FACE
Conforming.NSUM_EQ_0_IFF
Conforming.NEGLIGIBLE_AFF_GE_1_2
Conforming.MEASURABLE_AFF_GT_2_1_INTER_BALL
Conforming.MESURABLE_YFAN_INTER_BALL
Conforming.RADIAL_AFF_GE_1_2
Conforming.SOLID_ANGLE_YFAN
Conforming.SOL_UNIONS
Conforming.OPEN_TOPOLOGICAL_COMPONENT_YFAN_INTER_BALL
Conforming.SUM_SOL_IN_FACE_SET_EQ_4PI
Conforming.mono_cyclic_power_sigma_fan
Conforming.exists_face_in_face_set
Conforming.condition_aff_gt_subset_yfan
Conforming.SET_OF_EDGE_UNION_GRAPH
Conforming.SET_OF_EDGE_INVARIANT
Conforming.set_of_only_edge1
Conforming.azim_trangle_le_azim_face_fan
Conforming.f1_fan_of_f20_eq_f30
Conforming.card_ds2_fanadd_eq3
Conforming.TRANF
Conforming.TRAN_COMMUTATIVE_F1_FAN0
Conforming.INJ_TRANF_FACE_DELETE_DS
Conforming.EQ_CARD_FACE_FAN_AND_FANADD
Conforming.lemma_yfanadd_aff_ge
Conforming.INTERS_HALF_SPACE_DS_FANADD1
Conforming.lemmaINTERS_HALF_SPACE_DS_FANADD1
Conforming.SPACE3_EQ_UNION_3SET
Conforming.dartset_leads_into_ds_open_fanadd
Conforming.RADIAL_AFF_GT_1_2
Conforming.SOL_AFF_GT_2_1
Conforming.DS1_DS2_EQ_DS_FANADD
Conforming.conforming_diagonal_fanadd1
Conforming.DART_FANADD_SUBSET_HALFSPACE
Conforming.HYUAZSE
Conforming.NEGLIGIBLE_AFF_3_FAN
Conforming.exists_measure_ball_diff_set_negligible
Conforming.lemma_connect_hypermap
Polyhedron.POLYHEDRON_FAN
Polyhedron.RELATIVE_SUBSET_FCHANGE
Polyhedron.INTERIOR_AFFINIE_HUL_EQ_UNIV
Polyhedron.CARD_EXISTS_2
Polyhedron.FCHANGED_SUBSET_YFAN
Polyhedron.AMHFNXP_BIJ
Polyhedron.POLYTOPE_FAN80
Pack1.norm_abs
Pack1.KIUMVTC
Pack1.convex_nua_kg
Pack1.not_open_voronoi1
Pack1.DRUQUFE
Pack1.measurable_packing_lm2
Pack1.unions_voronoi_center_in_ball_subset_ball
Pack1.measure_unions_sum_voronoi
Pack2.VORONOI_CLOSED
Pack2.VORONOI_OPEN_AS_INTERSECTION
Pack2.BASE_IN_VORONOI_CLOSED
Pack2.MEASURABLE_VORONOI_CLOSED
Pack2.VORONOI_OPEN_SUBSET_CLOSED
Pack2.DRUQUFE
Pack2.finite_set_voronoi_center_in_ball
Packing3.PERMUTES_TRIVIAL
Packing3.HULL_INTERS_SUBSET_INTERS_HULL
Packing3.REAL_DIV_LE_1
Packing3.CLOSED_BIS_LE
Packing3.CLOSED_DISCRETE
Packing3.VORONOI_CLOSED_CONTAINS_BALL
Packing3.VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE
Packing3.INITIAL_SUBLIST_HEAD_EQ_2
Packing3.INITIAL_SUBLIST_EXISTS
Packing3.HD_IN_SET_OF_LIST
Packing3.LENGTH_LEFT_ACTION_LIST
Packing3.EL_DROP
Packing3.BARV_CONS
Packing3.TRUNCATE_0_EQ_HEAD
Packing3.LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST
Packing3.VORONOI_SET_2
Packing3.VORONOI_LIST_INTER_BIS
Packing3.MINIMAL_INTER_INTERS_EXISTS
Packing3.CONVEX_VORONOI_LIST
Packing3.OMEGA_LIST_N_IN_VORONOI_LIST
Rogers.REAL_NEG_LE_RMUL
Rogers.NUMSEG_SUBSET_INDUCT
Rogers.ODIGPXU
Rogers.OMEGA_LIST_N_EQ_GEN
Rogers.AFF_DIM_FINITE_UNION_LE
Rogers.UNIQUE_SOLUTION_lemma
Rogers.OAPVION3
Rogers.MHFTTZN_lemma
Rogers.ARCV_GT_PI2
Rogers.ANGLE_GT_PI2
Collect_geom.PER_SET3_conjunct1
Rogers.DIHV_LE_AZIM
Rogers.XYOFCGX
Rogers.AFFINE_HULL_PROJECTION_DIST_LE
Rogers.HL_PROPERTIES
Rogers.AFFINE_HULL_PROJECTION_SEPARATES
Rogers.WAUFCHE2
Rogers.AFFINE_HULL_VORONOI_LIST_SUBSET_INTERS_BIS
Rogers.KSOQKWL_lemma1
Tarjjuw.CHANGE_TARJJUW_1
Tarjjuw.CHANGE_TARJJUW_6
Marchal_cells.TRUNCATE_SIMPLEX_GENERAL_0
Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_3
Marchal_cells.OMEGA_LIST_3_EXPLICIT
Upfzbzm_support_lemmas.ZERO_LT_MM2_LEMMA
Upfzbzm_support_lemmas.FINITE_edgeX
Upfzbzm_support_lemmas.negligible_fun_any_C
Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT
Marchal_cells_2_new.CONVEX_HULL_4_SUBSET_AFF_GE_2_2
Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA
Marchal_cells_2_new.CLOSED_CONVEX_HULL_FINITE
Marchal_cells_2_new.MXI_EXPLICIT
Marchal_cells_2_new.OMEGA_LIST_TRUNCATE_2_NEW1
Marchal_cells_2_new.CONVEX_HULL_KY_LEMMA_5
Marchal_cells_2_new.INTER_RCONE_GE_IMP_BETWEEN_PROJ_POINT
Marchal_cells_2_new.NUMSEG_012
Trigonometry2.UV_IN_AFF2_conjunct0
Urrphbz1.MEASURABLE_MCELL
Rvfxzbu.RVFXZBU
Qzksykg.CONVEX_HULL_4_IMP_3_1
Ddzuphj.RCONE_GT_EQ_EMPTY_LEMMA
Qzyzmjc.mcell_set_2
Marchal_cells_3.ROGERS_SUBSET_VORONOI_CLOSED
Marchal_cells_3.PACKING_BALL_BOUNDARY
Marchal_cells_3.REAL_DIV_LE_1_TACTICS
Marchal_cells_3.LIFT_DIV_CONTINUOUS_ON
Marchal_cells_3.MCELL_SUBSET_BALL8_1
Marchal_cells_3.FINITE_LIST_KY_LEMMA_2
Marchal_cells_3.DIHX_LE_PI
Marchal_cells_3.MCELL_ID_MXI_2
Marchal_cells_3.gamma_y_pos_le
Marchal_cells_3.CARD_MCELL_CONTAINS_POINT_klemma
Marchal_cells_3.gamma_y_lmfun_bound2
Sum_gammax_lmfun_estimate.SUM_GAMMAX_LMFUN_ESTIMATE
Rdwkarc.PACKING_TRANS
Wrgcvdr_cizmrrh.ff_of_hyp2
Wrgcvdr_cizmrrh.UNI_E_IMP_EE_EQ_SET_OF_EDGE
Wrgcvdr_cizmrrh.FINITE_OF_N_FIRST_ELMS
Wrgcvdr_cizmrrh.CARD_N_FIRST_ELMS_UNDUCTIVE
Wrgcvdr_cizmrrh.ITER1
Wrgcvdr_cizmrrh.F_INVERSE_F_F
Wrgcvdr_cizmrrh.SLIDABLE_PROJECTION
Wrgcvdr_cizmrrh.PROJECT_EQ_VEC0_IMP_PARALLED
Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN
Wrgcvdr_cizmrrh.IN_E_IMP_IMP_IN_DARTS
Wrgcvdr_cizmrrh.IN_E_IFF_IN_ORD_E
Wrgcvdr_cizmrrh.ff_of_hyp3
Wrgcvdr_cizmrrh.HYP_LEMMA
Wrgcvdr_cizmrrh.ITER_AZIM_CYCLE_EQ_ITER_SIGMA
Wrgcvdr_cizmrrh.LOCAL_IMP_FINITE_DARTS
Wrgcvdr_cizmrrh.BIJ_BETWEEN_FF_AND_V
Wrgcvdr_cizmrrh.DIH2K_IMP_NODE_MAP_X_DIFF_X
Wrgcvdr_cizmrrh.CIZMRRH
Lvducxu.IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME
Lvducxu.LOCALIZE_PRESERVE_FACE
Lvducxu.CARD_E_GT1_EQ_CARD_E_PRIME
Lvducxu.CARD_FF_GT1_FF_SUBSET
Lvducxu.FX_IN_S_IMP_ORBIT_SUBSET
Lvducxu.EDGE_MAP_RESO_INVERSE_conjunct1
Lvducxu.DIH2K_IMP_SIMPLE_HYPERMAP2
Lvducxu.ENF_IMAGE_ITSELF_conjunct0
Ldurdpn.LDURDPN
Local_lemmas.COLLINEAR_CROSS_0
Local_lemmas.LOCAL_FAN_NOT_SING_FF
Local_lemmas.GRAPH_WITH_SET2
Local_lemmas.FINTE_OF_N_FIRST_ELMS2
Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE
Local_lemmas.MIXED_PROD_POS_IMP_RANGE_AZIM
Local_lemmas.RHO_NODE_IS_SUCCESEOR_AZIM
Local_lemmas.CARD_IMAGE_INJ2
Local_lemmas.IN_WEDGE_IMP_AZIM_LE
Local_lemmas.SELF_CYCLIC_IMP_FINITE
Local_lemmas.RHO_NODE_INVERSE_POINT
Local_lemmas.IN_CONV0
Local_lemmas.CONV02_SUBSET_AFF2
Local_lemmas.AFF_CONV0_COLL4
Local_lemmas.AFF2_ITR_CONV0_IMP_SAME_ENDS
Local_lemmas.lemma_in_orbit_iter
Local_lemmas.AFF_GT_LT_INTER_SYM
Local_lemmas.LEMMA_SUBSET_ORBIT_MAP_LT
Local_lemmas.AZIM_PI_WEDGE_GE_SIN
Local_lemmas.LOFA_IMP_NOT_INCLUDE_VEC0
Local_lemmas.PRE_IVS_RHO_NODE1_DETE
Local_lemmas.IN_AFF_LT_IMP_IN_CONV
Local_lemmas.AFF_GE_MONO_TRANS
Local_lemmas.LOFA_IMP_BIJ_FF_V
Local_lemmas.RHO_NODE1_MONO_WITH_AZIM
Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT
Local_lemmas.IN_CONV0_IMP_COLL_IFF
Local_lemmas.FOR_AFF_GT_NOT_INTERSECTION
Local_lemmas.USEFULL_THHM
Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2
Local_lemmas.HALP_CIRCLE_IS_INTERSECTION
Local_lemmas.DIHV_NOT_CHANGE
Local_lemmas.LOCAL_FAN_FINITE_V
Local_lemmas.PRIOR_TO_LESS_THAN_PI_LEMMA
Local_lemmas.DISJOINT_DOUBLE_SING
Local_lemmas.MONO_AZIM_AS_BTA_I
Local_lemmas.INSERT_UNION2
Nkezbfc_local.SOL_LOCAL_FAN_POS_CASE3
Nkezbfc_local.AZIM_PI_WEDGE_CROSS_DOT
Nkezbfc_local.PROPERTIES_AFF_GT_SUBSET_WEDGE
Arc_properties.HAS_REAL_DERIVATIVE_LOCAL
Arc_properties.SUM_PAIR_0
Arc_properties.arc_lemma3
Cfyxfty.GINGUAP
Cfyxfty.AFF_GE_3_1
Cfyxfty.SUBSET_EDGES0_FAN
Ysskqoy.CARD_UNION_EQ
Ysskqoy.COS_ARG_VECTOR_ANGLE
Ysskqoy.arc_length2_increasing
Counting_spheres.facet_rep_uniq_c
Counting_spheres.affine_facet_hyper
Counting_spheres.facet_rep_a_uniq
Counting_spheres.facet_rep_nz
Counting_spheres.XULJEPR_sum
Counting_spheres.g_convex
Counting_spheres.INJ_IMAGE
Counting_spheres.PACKING_INSERT
Counting_spheres.pad2d3d_dropout_lemma
Counting_spheres.ARG_ORDER
Dih2k_hypermap.DIMINDEX_HAS_SIZE_FINITE_PRODUCT
Dih2k_hypermap.LINEAR_VECMAT
Dih2k_hypermap.MATVEC_SUB
Dih2k_hypermap.CLOSED_MATVEC
Dih2k_hypermap.SUC_NOT
Dih2k_hypermap.AFF_INTER_AFF_GT_EQ_EMPTY
Dih2k_hypermap.LIM_VECMAT
Dih2k_hypermap.POINT_COM_AFF_GT_INTER
Dih2k_hypermap.MOD_IMP_EQ
Dih2k_hypermap.POWER_FF_HYP_ID
Dih2k_hypermap.NN_OF_HYP_EQ
Dih2k_hypermap.FINITE_F_SY
Dih2k_hypermap.FF_OF_HYP_EQ1
Dih2k_hypermap.ID_FF_OF_HYP_NOT_DARTS
Dih2k_hypermap.NODE_SY_POWER_ID
Dih2k_hypermap.DIH2K_FAN_HYP_SY
Tecoxbm.IVS_RHO_NODE_IN_EDGE
Hdplygy.MOD_EQ_MOD1
Hdplygy.CONTINUOUS_ON_D_FUN
Hdplygy.SEQUENTIALLY_DIVH
Hdplygy.CONTINUOUS_ON_TAU_STAR
Gbycpxs.SING_J1_SY
Mtuwlun.CARD_I_SY_LT_3
Mtuwlun.PMAT2_EQ_SY
Mtuwlun.ORDER_COVER1_SY
Mtuwlun.SLICEE_EQ_E2_SY
Tame_inequalities.main_lemma
Tame_inequalities.eta_x_ineq_lemma
Tame_inequalities.DIH_Y_INEQ
Ckqowsa_3_points.in_aff_ge_0_2
Ckqowsa_3_points.DIST_LOWER_BOUND_lemma
Ckqowsa_3_points.lemma_3_points
Ckqowsa_4_points.zero_not_between
Ckqowsa_4_points.PROJECTION_DIST2
Ckqowsa_4_points.aff_ge_0_2_SUBSET
Ckqowsa_4_points.rotation_dist_decrease_lemma
Ckqowsa_4_points.rotation_lemma_segments
Ckqowsa_4_points.continuous_lemma_aff_ge
Ckqowsa_4_points.lemma_4_points_rotation2_full
Ckqowsa.ESTD_fan1
Ckqowsa.fan7_4_1_one_case
Tame_general.DIFF_LEMMA
Tame_general.CONTRAVENING_DIST
Tame_general.CONTRAVENING_IMP_NOT_COPLANAR
Tame_opposite.tuple_opposite_hypermap
Tame_opposite.opposite_path
Tame_opposite.opposite_no_loops
Tame_opposite.CARD_nodes
Tame_opposite.the_SAME_type
Fatugpd.bdd_num_func_attain_max
Fatugpd.fourier
Fatugpd.dot_gt_0
Fatugpd.lemma5
Crttxat_tame.FACE_SUM_lemma
Hrxefdm_tame.tauVEF_alt2