Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (923 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (751 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (17 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (61 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (36 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (43 entries)

Global Index

A

AD [constructor, in AreaMethod.Rgeometry_tools]
advanced_parallel_lemmas [library]
AF [inductive, in AreaMethod.Rgeometry_tools]
AFinv [constructor, in AreaMethod.Rgeometry_tools]
AFmult [constructor, in AreaMethod.Rgeometry_tools]
AFopp [constructor, in AreaMethod.Rgeometry_tools]
AFplus [constructor, in AreaMethod.Rgeometry_tools]
AFvar [constructor, in AreaMethod.Rgeometry_tools]
AF0 [constructor, in AreaMethod.Rgeometry_tools]
AF1 [constructor, in AreaMethod.Rgeometry_tools]
AP [inductive, in AreaMethod.Rgeometry_tools]
APvar [constructor, in AreaMethod.Rgeometry_tools]
area_coords_constructions [library]
area_coords_elimination [library]
area_elimination_lemmas [library]
area_method [library]
AS [constructor, in AreaMethod.Rgeometry_tools]
aux [lemma, in AreaMethod.freepoints]
aux_co_side_4 [lemma, in AreaMethod.ratios_elimination_lemmas]
aux_co_side_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
aux_co_side_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
aux_co_side_3 [lemma, in AreaMethod.ratios_elimination_lemmas]
AVars [inductive, in AreaMethod.Rgeometry_tools]
a_ratio [definition, in AreaMethod.area_coords_constructions]
A1a [lemma, in AreaMethod.geometry_tools_lemmas]
A1b [axiom, in AreaMethod.chou_gao_zhang_axioms]
A2a [axiom, in AreaMethod.chou_gao_zhang_axioms]
A2b [axiom, in AreaMethod.chou_gao_zhang_axioms]
A2bgen [lemma, in AreaMethod.basic_geometric_facts]
A3a [axiom, in AreaMethod.chou_gao_zhang_axioms]
A3b [axiom, in AreaMethod.chou_gao_zhang_axioms]
A4 [axiom, in AreaMethod.chou_gao_zhang_axioms]
A5 [axiom, in AreaMethod.chou_gao_zhang_axioms]
A6 [axiom, in AreaMethod.chou_gao_zhang_axioms]
A6_6 [lemma, in AreaMethod.basic_geometric_facts]
A6_5 [lemma, in AreaMethod.basic_geometric_facts]
A6_2 [lemma, in AreaMethod.basic_geometric_facts]
A6_4 [lemma, in AreaMethod.basic_geometric_facts]
A6_3 [lemma, in AreaMethod.basic_geometric_facts]
A6_1 [lemma, in AreaMethod.basic_geometric_facts]


B

basic_geometric_facts [library]
bench_normalization_tactics [library]
build_point_not_collinear_1 [lemma, in AreaMethod.basic_geometric_facts]
build_point_not_collinear_2 [lemma, in AreaMethod.basic_geometric_facts]


C

centroid_midpoint_centroid_2 [lemma, in AreaMethod.examples_centroid]
centroid_check [lemma, in AreaMethod.examples_centroid]
centroid_midpoint_centroid [lemma, in AreaMethod.examples_centroid]
Ceva [lemma, in AreaMethod.examples_2]
chara_not_2 [axiom, in AreaMethod.chou_gao_zhang_axioms]
chasles [axiom, in AreaMethod.chou_gao_zhang_axioms]
check_co_circle [lemma, in AreaMethod.euclidean_constructions]
check_circumcenter [lemma, in AreaMethod.examples_circumcenter]
chou_gao_zhang_axioms [library]
circle_square_triangle [lemma, in AreaMethod.examples_6]
Col [definition, in AreaMethod.chou_gao_zhang_axioms]
col_4 [lemma, in AreaMethod.basic_geometric_facts]
col_par_4 [lemma, in AreaMethod.parallel_lemmas]
col_par_2 [lemma, in AreaMethod.parallel_lemmas]
col_2 [lemma, in AreaMethod.basic_geometric_facts]
col_par_par [lemma, in AreaMethod.parallel_lemmas]
col_decS [lemma, in AreaMethod.elimination_prepare]
col_not_col_1 [lemma, in AreaMethod.basic_geometric_facts]
col_5 [lemma, in AreaMethod.basic_geometric_facts]
col_par_3 [lemma, in AreaMethod.parallel_lemmas]
col_pyth [lemma, in AreaMethod.pythagoras_difference]
col_3 [lemma, in AreaMethod.basic_geometric_facts]
col_1 [lemma, in AreaMethod.basic_geometric_facts]
col_trans_1 [lemma, in AreaMethod.basic_geometric_facts]
col_dec [lemma, in AreaMethod.chou_gao_zhang_axioms]
col_par_1 [lemma, in AreaMethod.parallel_lemmas]
combine_inter_parallel [lemma, in AreaMethod.simplify_constructions]
common_point_not_par_aux [lemma, in AreaMethod.parallel_lemmas]
common_point_not_par [lemma, in AreaMethod.parallel_lemmas]
constructed_points_elimination [library]
construction_lemmas [library]
construction_lemmas_2 [library]
construction_tactics [library]
Conversemenelaus [lemma, in AreaMethod.examples_2]
ConverseMenelauseQuadri [lemma, in AreaMethod.examples_2]
co_side_bis [lemma, in AreaMethod.basic_geometric_facts]
co_side [lemma, in AreaMethod.basic_geometric_facts]
co_side_main [lemma, in AreaMethod.basic_geometric_facts]
co_side_elim_3 [lemma, in AreaMethod.ratios_elimination_lemmas]
co_side_elim_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
co_side_ter [lemma, in AreaMethod.basic_geometric_facts]
co_circle [definition, in AreaMethod.euclidean_constructions]
co_side_elim_4 [lemma, in AreaMethod.ratios_elimination_lemmas]
co_side_elim_1 [lemma, in AreaMethod.ratios_elimination_lemmas]


D

degenerated_ratio [lemma, in AreaMethod.geometry_tools_lemmas]
Desargues [lemma, in AreaMethod.examples_2]
Det3 [definition, in AreaMethod.freepoints]
diago_par_intersect [lemma, in AreaMethod.parallel_lemmas]
diag_mid_point_parallel [lemma, in AreaMethod.basic_geometric_facts]
diff_not_col_par_not_col [lemma, in AreaMethod.advanced_parallel_lemmas]
dirseg_simpl_1 [lemma, in AreaMethod.basic_geometric_facts]
dirseg_2 [lemma, in AreaMethod.basic_geometric_facts]
dirseg_3 [lemma, in AreaMethod.basic_geometric_facts]
dirseg_1 [lemma, in AreaMethod.basic_geometric_facts]
dirseg_simpl_2 [lemma, in AreaMethod.basic_geometric_facts]
dirseg_4 [lemma, in AreaMethod.basic_geometric_facts]
dirsur_1 [lemma, in AreaMethod.basic_geometric_facts]
divnonzero [lemma, in AreaMethod.field_general_properties]
DSeg [axiom, in AreaMethod.chou_gao_zhang_axioms]


E

egalcol [lemma, in AreaMethod.basic_geometric_facts]
egalzero [lemma, in AreaMethod.geometry_tools_lemmas]
elimination_prepare [library]
elim_py_inter_ll_right_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_left_right_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_line_middle [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_spec_a [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_left_right_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_length_ratio_inter_ll_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_py_midpoint_left_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_perp_d_middle [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_line_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_b [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_inter_line_parallel_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_spec_a [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_b [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_a_ratio_middle [lemma, in AreaMethod.area_coords_elimination]
elim_length_ratio_on_line_d_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_py_on_parallel_d_middle [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_a [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_middle_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_a [lemma, in AreaMethod.py_elimination_lemmas]
elim_signed_area_a_ratio [lemma, in AreaMethod.area_coords_elimination]
elim_ratio_on_perp_d_spec_b [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_foot_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_left_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_foot [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_perp_d_left_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_middle [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_line_d [lemma, in AreaMethod.area_elimination_lemmas]
elim_area_on_inter_parallel_parallel_RY [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_py_on_foot_middle [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_parallel [lemma, in AreaMethod.area_elimination_lemmas]
elim_area_inter_ll [lemma, in AreaMethod.area_elimination_lemmas]
elim_length_ratio_on_inter_parallel_parallel_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_a_aux [lemma, in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_line_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_foot_a_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_parallel_d_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_a_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_right_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_spec_b [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_b_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_line_d_middle [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_inter_parallel_parallel [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_line_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_area_on_perp_d [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_perp_d_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_line_d_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_length_ratio_inter_ll_1_spec [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_parallel_d_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_b_aux [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_parallel_d [lemma, in AreaMethod.area_elimination_lemmas]
elim_py_inter_ll_middle_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_on_line_d_left_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_py_a_ratio_right [lemma, in AreaMethod.area_coords_elimination]
elim_area_on_line [lemma, in AreaMethod.area_elimination_lemmas]
elim_length_ratio_inter_ll_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_py_on_parallel_d_left_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_line_d_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_b_auxi [lemma, in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_parallel_d_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_inter_ll_2_spec [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_inter_parallel_parallel_1 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_inter_line_parallel_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
elim_py_on_foot_left_right [lemma, in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_b_invariant [lemma, in AreaMethod.py_elimination_lemmas]
elim_area_on_inter_line_parallel [lemma, in AreaMethod.area_elimination_lemmas]
elim_py_a_ratio_left_right [lemma, in AreaMethod.area_coords_elimination]
eqF [definition, in AreaMethod.Rgeometry_tools]
eq_simpl_7 [lemma, in AreaMethod.area_method]
eq_simpl_3 [lemma, in AreaMethod.area_method]
eq_distance [definition, in AreaMethod.euclidean_constructions]
eq_simpl_6 [lemma, in AreaMethod.area_method]
eq_simpl_2 [lemma, in AreaMethod.area_method]
eq_simpl_1 [lemma, in AreaMethod.area_method]
eq_dec_points [lemma, in AreaMethod.chou_gao_zhang_axioms]
eq_simpl [lemma, in AreaMethod.my_field_tac]
eq_simpl_10 [lemma, in AreaMethod.area_method]
eq_simpl_9 [lemma, in AreaMethod.area_method]
eq_simpl_5 [lemma, in AreaMethod.area_method]
eq_simpl_8 [lemma, in AreaMethod.area_method]
eq_simpl_4 [lemma, in AreaMethod.area_method]
eq_half_eq_zero [lemma, in AreaMethod.pythagoras_difference_lemmas]
eq_diff_diff [lemma, in AreaMethod.basic_geometric_facts]
eq_angle [definition, in AreaMethod.euclidean_constructions]
eq_product [definition, in AreaMethod.euclidean_constructions]
essai [lemma, in AreaMethod.tests_elimination_tactics_py]
euclidean_constructions_2 [library]
euclidean_constructions [library]
euclid_parallel_existence_strong [lemma, in AreaMethod.basic_geometric_facts]
euclid_parallel_existence [lemma, in AreaMethod.basic_geometric_facts]
euler_line [lemma, in AreaMethod.examples_centroid]
examples_centroid [library]
examples_interactive [library]
examples_circumcenter [library]
examples_1 [library]
examples_2 [library]
examples_3 [library]
examples_4 [library]
examples_5 [library]
examples_6 [library]
example_construction_simplification [lemma, in AreaMethod.examples_1]
example6_9 [lemma, in AreaMethod.examples_3]
exercice2_38_3 [lemma, in AreaMethod.examples_3]
Exo55Hartsshorne [lemma, in AreaMethod.examples_2]
ex1_6auto [lemma, in AreaMethod.examples_2]


F

F [axiom, in AreaMethod.field]
Fdiv [definition, in AreaMethod.field]
Feq [definition, in AreaMethod.field]
field [library]
field_prop_5 [lemma, in AreaMethod.field_general_properties]
field_prop_3 [lemma, in AreaMethod.field_general_properties]
field_prop_1 [lemma, in AreaMethod.field_general_properties]
field_prop_2 [lemma, in AreaMethod.geometry_tools_lemmas]
field_prop_4 [lemma, in AreaMethod.field_general_properties]
field_prop1 [lemma, in AreaMethod.basic_geometric_facts]
field_general_properties [library]
field_variable_isolation_tactic [library]
Finv [axiom, in AreaMethod.field]
Finv_l [axiom, in AreaMethod.field]
Fminus [definition, in AreaMethod.field]
Fmult [axiom, in AreaMethod.field]
Fmult_assoc [axiom, in AreaMethod.field]
Fmult_sym [axiom, in AreaMethod.field]
Fmult_1l [axiom, in AreaMethod.field]
Fmult_Fplus_distr [axiom, in AreaMethod.field]
Fmult_Fplus_distr_r [lemma, in AreaMethod.field]
Fopp [axiom, in AreaMethod.field]
formula [inductive, in AreaMethod.Rgeometry_tools]
formula2 [inductive, in AreaMethod.Rgeometry_tools]
Fplus [axiom, in AreaMethod.field]
Fplus_Ol [axiom, in AreaMethod.field]
Fplus_assoc [axiom, in AreaMethod.field]
Fplus_sym [axiom, in AreaMethod.field]
Fplus_Fopp_r [axiom, in AreaMethod.field]
freepoints [library]
freepoint_elimination_aux [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_7 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_3 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_5 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_7_non_zero_denom [lemma, in AreaMethod.freepoints]
free_points_area_elimination [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_6_non_zero_denom [lemma, in AreaMethod.freepoints]
free_point_ratio_elimination_2 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_6 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_1 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_8 [lemma, in AreaMethod.freepoints]
free_points_ratio_elimination_4 [lemma, in AreaMethod.freepoints]
free_points_elimination [library]
FRth [lemma, in AreaMethod.field]
Fth [lemma, in AreaMethod.field]
FVar [constructor, in AreaMethod.Rgeometry_tools]
f_const [constructor, in AreaMethod.Rgeometry_tools]
f_imp2 [constructor, in AreaMethod.Rgeometry_tools]
f_neq [constructor, in AreaMethod.Rgeometry_tools]
f_equal2_sym [lemma, in AreaMethod.area_method]
f_imp [constructor, in AreaMethod.Rgeometry_tools]
f_eq [constructor, in AreaMethod.Rgeometry_tools]
F0 [axiom, in AreaMethod.field]
F1 [axiom, in AreaMethod.field]
F1_neq_F0 [axiom, in AreaMethod.field]


G

gauss_line [lemma, in AreaMethod.examples_2]
general_tactics [library]
geometry_tools [library]
geometry_tools_lemmas [library]


H

half [lemma, in AreaMethod.geometry_tools]
harmonic [definition, in AreaMethod.euclidean_constructions]
herron_qin [lemma, in AreaMethod.pythagoras_difference_lemmas]


I

implies [definition, in AreaMethod.Rgeometry_tools]
interp_formula2_to_prop [definition, in AreaMethod.Rgeometry_tools]
interp_AF_to_F [definition, in AreaMethod.Rgeometry_tools]
interp_AP_to_Point [definition, in AreaMethod.Rgeometry_tools]
interp_f [definition, in AreaMethod.Rgeometry_tools]
inter_lc [definition, in AreaMethod.euclidean_constructions]
inter_ll_comm4 [lemma, in AreaMethod.ratios_elimination_lemmas]
inter_llex [lemma, in AreaMethod.construction_lemmas]
inter_ll_comm1 [lemma, in AreaMethod.ratios_elimination_lemmas]
inter_ll [definition, in AreaMethod.construction_lemmas]
inter_ll_ex [lemma, in AreaMethod.construction_lemmas]
inter_ll_comm2 [lemma, in AreaMethod.ratios_elimination_lemmas]
inter_ll_comm3 [lemma, in AreaMethod.ratios_elimination_lemmas]
inter_unicity_2 [lemma, in AreaMethod.basic_geometric_facts]
inter_unicity [lemma, in AreaMethod.basic_geometric_facts]
invariant_par_on_line_d_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_d_1_length_ratio_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_div_3 [lemma, in AreaMethod.my_field_tac]
invariant_par_on_parallel_d_1_length_ratio_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_d_1_length_ratio_3 [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_inverse_ratio [lemma, in AreaMethod.elimination_prepare]
invariant_par_on_line_1_length_ratio_3 [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_1_length_ratio_2 [lemma, in AreaMethod.ratios_elimination_lemmas]
invariant_div_1 [lemma, in AreaMethod.my_field_tac]
invariant_par_on_parallel_d_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
inverse_ratio [lemma, in AreaMethod.field_general_properties]
inversion [definition, in AreaMethod.euclidean_constructions]
is_orthocenter_non_zero' [lemma, in AreaMethod.area_coords_constructions]
is_circumcenter_non_zero [lemma, in AreaMethod.area_coords_constructions]
is_orthocenter_equiv [lemma, in AreaMethod.area_coords_constructions]
is_circumcenter_non_zero' [lemma, in AreaMethod.area_coords_constructions]
is_circumcenter [definition, in AreaMethod.area_coords_constructions]
is_orthocenter_non_zero [lemma, in AreaMethod.area_coords_constructions]
is_circumcenter' [definition, in AreaMethod.area_coords_constructions]
is_Lemoine [definition, in AreaMethod.area_coords_constructions]
is_midpoint [definition, in AreaMethod.construction_lemmas]
is_midpoint_A [lemma, in AreaMethod.examples_2]
is_orthocenter [definition, in AreaMethod.area_coords_constructions]
is_orthocenter' [definition, in AreaMethod.area_coords_constructions]
is_circumcenter_equiv [lemma, in AreaMethod.area_coords_constructions]
is_centroid [definition, in AreaMethod.area_coords_constructions]


L

lambda_zero_on_parallel_d [lemma, in AreaMethod.ratios_elimination_lemmas]
Lc [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcdiv1 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcdiv2 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcinv [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcmult1 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcmult2 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcm1 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcm2 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcop1 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcp1 [lemma, in AreaMethod.field_variable_isolation_tactic]
Lcp2 [lemma, in AreaMethod.field_variable_isolation_tactic]
ldiff [lemma, in AreaMethod.geometry_tools_lemmas]
list_assoc_inv [definition, in AreaMethod.Rgeometry_tools]
lpar1 [lemma, in AreaMethod.geometry_tools_lemmas]
lpar2 [lemma, in AreaMethod.geometry_tools_lemmas]
lpar3 [lemma, in AreaMethod.geometry_tools_lemmas]
l_27_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_3_4 [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_3_40 [lemma, in AreaMethod.examples_6]
l_6_271 [lemma, in AreaMethod.examples_6]
l_25_c [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_6_295 [lemma, in AreaMethod.examples_interactive]
l_28_a [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_3_4_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_24_c_on_foot [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_25_a [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_6_268 [lemma, in AreaMethod.examples_6]
l_6_267 [lemma, in AreaMethod.examples_6]
l_6_264 [lemma, in AreaMethod.examples_6]
l_6_273 [lemma, in AreaMethod.examples_interactive]
l_6_266 [lemma, in AreaMethod.examples_6]
l_6_134 [lemma, in AreaMethod.examples_6]
l_6_272 [lemma, in AreaMethod.examples_6]
l_6_269 [lemma, in AreaMethod.examples_6]
l_3_41 [lemma, in AreaMethod.examples_6]
l_6_270 [lemma, in AreaMethod.examples_6]
l_28_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_27_a [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_6_265 [lemma, in AreaMethod.examples_6]
l_6_191 [lemma, in AreaMethod.examples_interactive]
l_28_midpoint [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_24_a [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_28_b_midpoint [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_24_c [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_25_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_27_c [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_24_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l_3_45 [lemma, in AreaMethod.examples_6]
l1_24 [lemma, in AreaMethod.parallel_lemmas]
l1_25_aux [lemma, in AreaMethod.advanced_parallel_lemmas]
l1_25 [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_11a [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_12b [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_11a_strong [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_11b_strong_strong [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_9 [lemma, in AreaMethod.basic_geometric_facts]
l2_11b_strong_strong_strong [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_11b [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_12b_strong_3 [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_12a [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_9aux [lemma, in AreaMethod.basic_geometric_facts]
l2_15 [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_11a_strong_strong [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_7 [lemma, in AreaMethod.basic_geometric_facts]
l2_11a_strong_strong_strong [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_12a_strong_3 [lemma, in AreaMethod.advanced_parallel_lemmas]
l2_9_weak [lemma, in AreaMethod.basic_geometric_facts]
l2_11a_strong_strong_strong_aux [lemma, in AreaMethod.advanced_parallel_lemmas]
l3_6_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_8_a [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_6 [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_43 [lemma, in AreaMethod.examples_2]
l3_44 [lemma, in AreaMethod.examples_3]
l3_10 [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_8_b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_9 [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_10b [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_5_py [lemma, in AreaMethod.pythagoras_difference_lemmas]
l3_51 [lemma, in AreaMethod.examples_6]
l3_9_aux [lemma, in AreaMethod.pythagoras_difference_lemmas]
l6_44 [lemma, in AreaMethod.examples_6]
l6_47 [lemma, in AreaMethod.examples_centroid]
l6_196 [lemma, in AreaMethod.examples_circumcenter]
l6_86 [lemma, in AreaMethod.examples_circumcenter]
l6_90 [lemma, in AreaMethod.examples_circumcenter]
l6_224 [lemma, in AreaMethod.examples_5]
l6_217 [lemma, in AreaMethod.examples_2]
l6_46 [lemma, in AreaMethod.examples_6]
l6_17 [lemma, in AreaMethod.examples_5]
l6_144 [lemma, in AreaMethod.examples_interactive]
l6_52 [lemma, in AreaMethod.examples_5]
l6_69 [lemma, in AreaMethod.examples_5]
l6_56 [lemma, in AreaMethod.examples_5]
l6_17 [lemma, in AreaMethod.examples_6]
l6_95 [lemma, in AreaMethod.examples_circumcenter]
l6_44 [lemma, in AreaMethod.examples_centroid]
l6_84 [lemma, in AreaMethod.examples_6]
l6_88 [lemma, in AreaMethod.examples_circumcenter]
l6_87 [lemma, in AreaMethod.examples_circumcenter]
l6_223 [lemma, in AreaMethod.examples_5]
l6_63 [lemma, in AreaMethod.examples_interactive]
l6_67 [lemma, in AreaMethod.examples_5]
l6_15 [lemma, in AreaMethod.examples_interactive]
l6_55 [lemma, in AreaMethod.examples_5]
l6_197 [lemma, in AreaMethod.examples_5]
l6_222 [lemma, in AreaMethod.examples_6]
l6_218 [lemma, in AreaMethod.examples_5]


M

Menelaus [lemma, in AreaMethod.examples_2]
MenelausQuadri [lemma, in AreaMethod.examples_2]
midpoint_ratio_1 [lemma, in AreaMethod.pythagoras_difference_lemmas]
midpoint_elim [lemma, in AreaMethod.examples_interactive]
midpoint_on_line_d [lemma, in AreaMethod.pythagoras_difference_lemmas]
midpoint_is_midpoint [lemma, in AreaMethod.pythagoras_difference_lemmas]
midpoint_ratio_2 [lemma, in AreaMethod.pythagoras_difference_lemmas]
mid_point_degenerated_1 [lemma, in AreaMethod.basic_geometric_facts]
mid_point_ex [lemma, in AreaMethod.basic_geometric_facts]
mid_point_comm [lemma, in AreaMethod.basic_geometric_facts]
mid_point [definition, in AreaMethod.basic_geometric_facts]
mid_point_equation [lemma, in AreaMethod.parallel_lemmas]
mid_point_degenerated_2 [lemma, in AreaMethod.basic_geometric_facts]
mid_point_degenerated_3 [lemma, in AreaMethod.basic_geometric_facts]
mratio [definition, in AreaMethod.construction_lemmas]
multnonzero [lemma, in AreaMethod.field_general_properties]
multnonzero_r [lemma, in AreaMethod.field_general_properties]
multnonzero_l [lemma, in AreaMethod.field_general_properties]
my_field_tac [library]
m_ratio [definition, in AreaMethod.euclidean_constructions]


N

nateq [definition, in AreaMethod.Rgeometry_tools]
nateq_prop [lemma, in AreaMethod.Rgeometry_tools]
natle [definition, in AreaMethod.Rgeometry_tools]
neqF [definition, in AreaMethod.Rgeometry_tools]
neq_not_zero [lemma, in AreaMethod.geometry_tools_lemmas]
nine_point_1 [lemma, in AreaMethod.examples_6]
nonzerodiv [lemma, in AreaMethod.field_general_properties]
nonzeroinv [lemma, in AreaMethod.field_general_properties]
nonzeromult [lemma, in AreaMethod.field_general_properties]
non_zero_denom_on_inter_parallel_parallel_area [lemma, in AreaMethod.area_elimination_lemmas]
non_zero_denom_on_line_2_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_d_2_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_inter_line_parallel_area [lemma, in AreaMethod.area_elimination_lemmas]
non_zero_denom_on_parallel_d_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_d_1_length_ratio_seg [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_area [lemma, in AreaMethod.area_elimination_lemmas]
non_zero_denom_on_line_1_length_ratio_seg [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_parallel_d_area [lemma, in AreaMethod.area_elimination_lemmas]
non_zero_denom_inter_ll_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_parallel_d_2_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_inter_ll_2_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_d_1_length_ratio [lemma, in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_inter_ll_area [lemma, in AreaMethod.area_elimination_lemmas]
notcolnotegal_2 [lemma, in AreaMethod.basic_geometric_facts]
notcolnotegal_1 [lemma, in AreaMethod.basic_geometric_facts]
notcolnotegal_3 [lemma, in AreaMethod.basic_geometric_facts]
noteqnotzero [lemma, in AreaMethod.basic_geometric_facts]
notparallelnotegal_1 [lemma, in AreaMethod.basic_geometric_facts]
notparallelnotegal_2 [lemma, in AreaMethod.basic_geometric_facts]
not_para_eq_4 [lemma, in AreaMethod.parallel_lemmas]
not_eq_py_not_zero [lemma, in AreaMethod.pythagoras_difference]
not_para_eq_2 [lemma, in AreaMethod.parallel_lemmas]
not_parallel_not_eq_1 [lemma, in AreaMethod.basic_geometric_facts]
not_para_eq_3 [lemma, in AreaMethod.parallel_lemmas]
not_para_eq_1 [lemma, in AreaMethod.parallel_lemmas]
not_parallel_not_eq_2 [lemma, in AreaMethod.basic_geometric_facts]
not_para_eq_5 [lemma, in AreaMethod.parallel_lemmas]
not_perp_to_itself [lemma, in AreaMethod.pythagoras_difference_lemmas]
not_para_eq_6 [lemma, in AreaMethod.parallel_lemmas]
nuldirseg [lemma, in AreaMethod.geometry_tools_lemmas]
number_dec [lemma, in AreaMethod.chou_gao_zhang_axioms]


O

on_inter_parallel_parallel_ex [lemma, in AreaMethod.construction_lemmas_2]
on_inter_parallel_parallel [definition, in AreaMethod.construction_lemmas]
on_line_dex_spec [lemma, in AreaMethod.advanced_parallel_lemmas]
on_perp_d [definition, in AreaMethod.euclidean_constructions]
on_line_dex_spec_strong_f [lemma, in AreaMethod.advanced_parallel_lemmas]
on_foot_per [lemma, in AreaMethod.pythagoras_difference_lemmas]
on_line_d [definition, in AreaMethod.construction_lemmas]
on_line_dex_spec_strong_bis [lemma, in AreaMethod.advanced_parallel_lemmas]
on_inter_line_parallel [definition, in AreaMethod.construction_lemmas]
on_circle [definition, in AreaMethod.euclidean_constructions]
on_line_to_on_line_d [lemma, in AreaMethod.construction_lemmas]
on_parallel_d [definition, in AreaMethod.construction_lemmas]
on_line_dex_spec_strong_ter [lemma, in AreaMethod.advanced_parallel_lemmas]
on_parallel_d_ex [lemma, in AreaMethod.construction_lemmas]
on_parallelex [lemma, in AreaMethod.construction_lemmas]
on_parallel_ex [lemma, in AreaMethod.construction_lemmas]
on_perp_d_ex [lemma, in AreaMethod.euclidean_constructions_2]
on_line [definition, in AreaMethod.construction_lemmas]
on_perp [definition, in AreaMethod.euclidean_constructions]
on_parallel [definition, in AreaMethod.construction_lemmas]
on_line_dex [lemma, in AreaMethod.construction_lemmas]
on_perp_to_on_perp_d [lemma, in AreaMethod.euclidean_constructions]
on_foot_area_paper [lemma, in AreaMethod.pythagoras_difference]
on_line_dex_spec_strong [lemma, in AreaMethod.advanced_parallel_lemmas]
on_inter_line_parallel_ex [lemma, in AreaMethod.construction_lemmas_2]
on_foot_area [axiom, in AreaMethod.pythagoras_difference]
on_line_ex [lemma, in AreaMethod.construction_lemmas]
on_line_iff_on_parallel [lemma, in AreaMethod.euclidean_constructions]
on_lineex [lemma, in AreaMethod.construction_lemmas]
on_parallel_to_on_parallel_d [lemma, in AreaMethod.construction_lemmas]
on_inter_parallel_parallel_ex_aux [lemma, in AreaMethod.construction_lemmas_2]
on_inter_line_perp [definition, in AreaMethod.euclidean_constructions]
on_foot [definition, in AreaMethod.pythagoras_difference]
on_line_d_iff_on_parallel_d [lemma, in AreaMethod.euclidean_constructions]
opzero [lemma, in AreaMethod.field_general_properties]


P

Pappus [lemma, in AreaMethod.examples_4]
Pappus_2 [lemma, in AreaMethod.examples_4]
parallel [definition, in AreaMethod.chou_gao_zhang_axioms]
parallellogram_construction_2 [lemma, in AreaMethod.examples_1]
parallellogram_construction [lemma, in AreaMethod.examples_1]
parallellogram_second_parallel [lemma, in AreaMethod.examples_1]
parallelogram [definition, in AreaMethod.parallel_lemmas]
parallelogram_weak_3_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]
parallelogram_weak_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]
parallelogram_midpoint [lemma, in AreaMethod.examples_1]
parallel_side_eq_parallel [axiom, in AreaMethod.chou_gao_zhang_axioms]
parallel_equiv [lemma, in AreaMethod.area_method]
parallel_not_perp [lemma, in AreaMethod.pythagoras_difference_lemmas]
parallel_dec [lemma, in AreaMethod.chou_gao_zhang_axioms]
parallel_transitivity [lemma, in AreaMethod.examples_1]
parallel_transitivity [lemma, in AreaMethod.area_elimination_lemmas]
parallel_side_eq_weak_para [lemma, in AreaMethod.advanced_parallel_lemmas]
parallel_s [definition, in AreaMethod.area_method]
parallel_side_eq_weak_weak_para [lemma, in AreaMethod.advanced_parallel_lemmas]
parallel_side_eq_weak_weak_weak_para [lemma, in AreaMethod.advanced_parallel_lemmas]
parallel_side_eq_parallel' [lemma, in AreaMethod.basic_geometric_facts]
parallel_dec [lemma, in AreaMethod.freepoints]
parallel_pseudo_transitivity [lemma, in AreaMethod.examples_1]
parallel_lemmas [library]
para_1 [lemma, in AreaMethod.parallel_lemmas]
para_not_col_1 [lemma, in AreaMethod.parallel_lemmas]
para_not_eq_4 [lemma, in AreaMethod.parallel_lemmas]
para_not_eq_3 [lemma, in AreaMethod.parallel_lemmas]
para_not_col_3 [lemma, in AreaMethod.parallel_lemmas]
para_4 [lemma, in AreaMethod.parallel_lemmas]
para_2 [lemma, in AreaMethod.parallel_lemmas]
para_not_eq_6 [lemma, in AreaMethod.parallel_lemmas]
para_not_eq_5 [lemma, in AreaMethod.parallel_lemmas]
para_not_col_2 [lemma, in AreaMethod.parallel_lemmas]
para_not_eq_2 [lemma, in AreaMethod.parallel_lemmas]
para_not_eq_1 [lemma, in AreaMethod.parallel_lemmas]
para_3 [lemma, in AreaMethod.parallel_lemmas]
par_col_col_1 [lemma, in AreaMethod.parallel_lemmas]
par_not_all_col [lemma, in AreaMethod.basic_geometric_facts]
par_2 [lemma, in AreaMethod.basic_geometric_facts]
par_col_col_2 [lemma, in AreaMethod.parallel_lemmas]
par_1 [lemma, in AreaMethod.basic_geometric_facts]
par_col_col_4 [lemma, in AreaMethod.parallel_lemmas]
par_col_col_3 [lemma, in AreaMethod.parallel_lemmas]
par_aux_1 [lemma, in AreaMethod.basic_geometric_facts]
Pascal [lemma, in AreaMethod.examples_2]
pascalian_ax [lemma, in AreaMethod.advanced_parallel_lemmas]
per [definition, in AreaMethod.pythagoras_difference]
perp [definition, in AreaMethod.pythagoras_difference]
perp_9 [lemma, in AreaMethod.pythagoras_difference]
perp_bissect_perp [lemma, in AreaMethod.examples_6]
perp_para_perp [axiom, in AreaMethod.pythagoras_difference]
perp_bissect_eq_distance [lemma, in AreaMethod.examples_6]
perp_1 [lemma, in AreaMethod.pythagoras_difference]
perp_4 [lemma, in AreaMethod.pythagoras_difference]
perp_not_eq_not_perp [lemma, in AreaMethod.pythagoras_difference_lemmas]
perp_8 [lemma, in AreaMethod.pythagoras_difference]
perp_col_perp [lemma, in AreaMethod.pythagoras_difference_lemmas]
perp_6 [lemma, in AreaMethod.pythagoras_difference]
perp_3 [lemma, in AreaMethod.pythagoras_difference]
perp_5 [lemma, in AreaMethod.pythagoras_difference]
perp_2 [lemma, in AreaMethod.pythagoras_difference]
perp_bissect_eq_angle [lemma, in AreaMethod.examples_6]
perp_7 [lemma, in AreaMethod.pythagoras_difference]
perp_perp_para [axiom, in AreaMethod.pythagoras_difference]
perp_not_parallel [lemma, in AreaMethod.pythagoras_difference_lemmas]
perp4_perp [lemma, in AreaMethod.pythagoras_difference_lemmas]
per_dec [lemma, in AreaMethod.pythagoras_difference_lemmas]
per_col_eq [lemma, in AreaMethod.pythagoras_difference_lemmas]
per_area [lemma, in AreaMethod.pythagoras_difference_lemmas]
Point [axiom, in AreaMethod.chou_gao_zhang_axioms]
proj_ex [lemma, in AreaMethod.euclidean_constructions]
Prop51Hartsshorne [lemma, in AreaMethod.examples_2]
Prop51Hartsshornebis [lemma, in AreaMethod.examples_1]
Prop51Hartsshornebis [lemma, in AreaMethod.examples_2]
Prop54Hartsshorne [lemma, in AreaMethod.examples_2]
PVar [constructor, in AreaMethod.Rgeometry_tools]
Py [definition, in AreaMethod.pythagoras_difference]
pythagoras_difference [library]
pythagoras_difference_lemmas [library]
pyth_sym [lemma, in AreaMethod.pythagoras_difference]
pyth_simpl_4 [lemma, in AreaMethod.pythagoras_difference]
pyth_simpl_3 [lemma, in AreaMethod.pythagoras_difference]
pyth_simpl_1 [lemma, in AreaMethod.pythagoras_difference]
pyth_simpl_2 [lemma, in AreaMethod.pythagoras_difference]
py_zero_eq [lemma, in AreaMethod.pythagoras_difference]
py_elimination_lemmas [library]
Py4 [definition, in AreaMethod.pythagoras_difference]
py4_6 [lemma, in AreaMethod.pythagoras_difference]
py4_3 [lemma, in AreaMethod.pythagoras_difference]
py4_simpl_4 [lemma, in AreaMethod.pythagoras_difference]
py4_7 [lemma, in AreaMethod.pythagoras_difference]
py4_simpl_2 [lemma, in AreaMethod.pythagoras_difference]
py4_simpl_3 [lemma, in AreaMethod.pythagoras_difference]
py4_4 [lemma, in AreaMethod.pythagoras_difference]
py4_simpl_5 [lemma, in AreaMethod.pythagoras_difference]
py4_1 [lemma, in AreaMethod.pythagoras_difference]
py4_5 [lemma, in AreaMethod.pythagoras_difference]
py4_simpl_6 [lemma, in AreaMethod.pythagoras_difference]
py4_2 [lemma, in AreaMethod.pythagoras_difference]
py4_simpl_1 [lemma, in AreaMethod.pythagoras_difference]


R

ratios_elimination_lemmas [library]
rectangle_1 [lemma, in AreaMethod.examples_6]
rectangle_3 [lemma, in AreaMethod.examples_6]
rectangle_2 [lemma, in AreaMethod.examples_6]
remove_opp [lemma, in AreaMethod.my_field_tac]
remove_inv [lemma, in AreaMethod.my_field_tac]
Rgeometry_tools [library]


S

S [axiom, in AreaMethod.chou_gao_zhang_axioms]
same_denom_div_2 [lemma, in AreaMethod.my_field_tac]
same_denom_mul_2 [lemma, in AreaMethod.my_field_tac]
same_denom_min_2 [lemma, in AreaMethod.my_field_tac]
same_denom_add_3 [lemma, in AreaMethod.my_field_tac]
same_denom_add_2 [lemma, in AreaMethod.my_field_tac]
same_denom_conclude_2 [lemma, in AreaMethod.my_field_tac]
same_denom_min_1 [lemma, in AreaMethod.my_field_tac]
same_denom_add_1 [lemma, in AreaMethod.my_field_tac]
same_denom_conclude_4 [lemma, in AreaMethod.my_field_tac]
same_denom_div_1 [lemma, in AreaMethod.my_field_tac]
same_denom_mul_3 [lemma, in AreaMethod.my_field_tac]
same_denom_conclude_5 [lemma, in AreaMethod.my_field_tac]
same_denom_mul_1 [lemma, in AreaMethod.my_field_tac]
same_denom_conclude_3 [lemma, in AreaMethod.my_field_tac]
same_denom_div_3 [lemma, in AreaMethod.my_field_tac]
same_denom_conclude_1 [lemma, in AreaMethod.my_field_tac]
same_denom_min_3 [lemma, in AreaMethod.my_field_tac]
simplif [definition, in AreaMethod.Rgeometry_tools]
simplify_constructions [library]
simplif_correct [lemma, in AreaMethod.Rgeometry_tools]
simplring1 [lemma, in AreaMethod.geometry_tools_lemmas]
simp_frac_4 [lemma, in AreaMethod.my_field_tac]
simp_9 [lemma, in AreaMethod.my_field_tac]
simp_frac_5 [lemma, in AreaMethod.my_field_tac]
simp_frac_9 [lemma, in AreaMethod.my_field_tac]
simp_frac_7 [lemma, in AreaMethod.my_field_tac]
simp_frac_10 [lemma, in AreaMethod.my_field_tac]
simp_frac_6 [lemma, in AreaMethod.my_field_tac]
simp_2 [lemma, in AreaMethod.my_field_tac]
simp_7 [lemma, in AreaMethod.my_field_tac]
simp_frac_2 [lemma, in AreaMethod.my_field_tac]
simp_5 [lemma, in AreaMethod.my_field_tac]
simp_frac_16 [lemma, in AreaMethod.my_field_tac]
simp_frac_15 [lemma, in AreaMethod.my_field_tac]
simp_4 [lemma, in AreaMethod.my_field_tac]
simp_13 [lemma, in AreaMethod.my_field_tac]
simp_frac_16_inv [lemma, in AreaMethod.my_field_tac]
simp_1 [lemma, in AreaMethod.my_field_tac]
simp_frac_12 [lemma, in AreaMethod.my_field_tac]
simp_14 [lemma, in AreaMethod.my_field_tac]
simp_frac_3 [lemma, in AreaMethod.my_field_tac]
simp_12 [lemma, in AreaMethod.my_field_tac]
simp_10 [lemma, in AreaMethod.my_field_tac]
simp_frac_11 [lemma, in AreaMethod.my_field_tac]
simp_frac_1 [lemma, in AreaMethod.my_field_tac]
simp_11 [lemma, in AreaMethod.my_field_tac]
simp_8 [lemma, in AreaMethod.my_field_tac]
simp_3 [lemma, in AreaMethod.my_field_tac]
simp_frac_8 [lemma, in AreaMethod.my_field_tac]
simp_frac_13 [lemma, in AreaMethod.my_field_tac]
simp_6 [lemma, in AreaMethod.my_field_tac]
simp_frac_14 [lemma, in AreaMethod.my_field_tac]
simp_15 [lemma, in AreaMethod.my_field_tac]
SomePoint [axiom, in AreaMethod.Rgeometry_tools]
SomeValue [axiom, in AreaMethod.Rgeometry_tools]
square_1 [lemma, in AreaMethod.examples_6]
square_2 [lemma, in AreaMethod.examples_6]
square_to_py [lemma, in AreaMethod.pythagoras_difference]
symmetric_point_ex [lemma, in AreaMethod.basic_geometric_facts]
symmetric_point_unicity [lemma, in AreaMethod.pythagoras_difference_lemmas]
symmetric_point [definition, in AreaMethod.basic_geometric_facts]
S_4 [lemma, in AreaMethod.geometry_tools_lemmas]
S_3 [lemma, in AreaMethod.geometry_tools_lemmas]
S_1 [lemma, in AreaMethod.geometry_tools_lemmas]
S_0 [lemma, in AreaMethod.geometry_tools_lemmas]
S_2 [lemma, in AreaMethod.geometry_tools_lemmas]
S4 [definition, in AreaMethod.chou_gao_zhang_axioms]
S4Simpl_2 [lemma, in AreaMethod.geometry_tools]
S4Simpl_3 [lemma, in AreaMethod.geometry_tools]
S4Simpl_6 [lemma, in AreaMethod.geometry_tools]
S4Simpl_1 [lemma, in AreaMethod.geometry_tools]
S4Simpl_5 [lemma, in AreaMethod.geometry_tools]
S4Simpl_4 [lemma, in AreaMethod.geometry_tools]
S4_6 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_1 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_4 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_8 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_3 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_2 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_7 [lemma, in AreaMethod.geometry_tools_lemmas]
S4_5 [lemma, in AreaMethod.geometry_tools_lemmas]


T

tangent [definition, in AreaMethod.euclidean_constructions]
tests_elimination_tactics_ratios [library]
tests_elimination_tactics_areas [library]
tests_elimination_tactics_py [library]
test_uniformize_dir_seg_1 [lemma, in AreaMethod.geometry_tools]
test_area_on_parallel_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_on_parallel_d_1 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_foot_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_1 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_inter_ll_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_d_5 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_only_use_area_coordinates_1 [lemma, in AreaMethod.free_points_elimination]
test_on_line_d_12 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_3 [lemma, in AreaMethod.elimination_prepare]
test_on_line_d_11 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_parallel_3 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_1b [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_uniformize_dir_seg_2 [lemma, in AreaMethod.geometry_tools]
test_simpl_left_right_3 [lemma, in AreaMethod.area_method]
test_inter_ll_gen_3 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_line_d_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_gen_2 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_inter_ll_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_on_line_d_3 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_2b [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_on_line_4 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_line_d_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_on_inter_parallel_parallel_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_uniformize_dir_seg_4 [lemma, in AreaMethod.geometry_tools]
test_inter_ll_gen_1 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_d_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_parallel_d_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_parallel_d_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_on_parallel_d_3 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_area_on_perp_d_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_foot_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_5 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_perp_d_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_inter_ll_3 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_2 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_inter_ll_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_on_line_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_area_on_perp_d_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_line_d_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_2 [lemma, in AreaMethod.elimination_prepare]
test_py_on_parallel_d_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_1 [lemma, in AreaMethod.elimination_prepare]
test_area_on_perp_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_line_4_c [lemma, in AreaMethod.tests_elimination_tactics_py]
test_uniformize_dir_seg_5 [lemma, in AreaMethod.geometry_tools]
test_inter_ll_4 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_foot_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_6 [lemma, in AreaMethod.elimination_prepare]
test_area_on_parallel_d_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_area_on_line_3 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_simpl [lemma, in AreaMethod.pythagoras_difference]
test_on_foot_1 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_d_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_d_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_on_line_d_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_area_on_parallel_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_foot_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_check_ratio_hyp [lemma, in AreaMethod.area_method]
test_area_on_perp_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_3 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_area_inter_ll_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_on_foot_2 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_elim [lemma, in AreaMethod.examples_6]
test_py_on_line_d_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_inter_ll_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_perp_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_only_use_area_coordinates_3 [lemma, in AreaMethod.free_points_elimination]
test_py_on_line_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_inter_ll [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_foot_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_foot_5 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_perp_d_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_4_b [lemma, in AreaMethod.tests_elimination_tactics_py]
test_uniformize_dir_seg_3 [lemma, in AreaMethod.geometry_tools]
test_inter_ll_4b [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_inter_line_parallel_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_py_on_parallel_d_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_simpl_left_right_2 [lemma, in AreaMethod.area_method]
test_py_on_line_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_only_use_area_coordinates_2 [lemma, in AreaMethod.free_points_elimination]
test_inter_ll_3b [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_line_d_6 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_uniformize_pys [lemma, in AreaMethod.pythagoras_difference]
test_py_on_foot_4 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_1 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_4 [lemma, in AreaMethod.elimination_prepare]
test_inter_ll_5 [lemma, in AreaMethod.tests_elimination_tactics_ratios]
test_inter_ll_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_py_on_perp_3 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_simpl_left_right_1 [lemma, in AreaMethod.area_method]
test_basic_simpl [lemma, in AreaMethod.pythagoras_difference]
test_area_on_line_2 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test_5 [lemma, in AreaMethod.elimination_prepare]
test_py_on_line_2 [lemma, in AreaMethod.tests_elimination_tactics_py]
test_area_on_parallel_d_1 [lemma, in AreaMethod.tests_elimination_tactics_areas]
test1 [lemma, in AreaMethod.bench_normalization_tactics]
test10 [lemma, in AreaMethod.bench_normalization_tactics]
test11 [lemma, in AreaMethod.bench_normalization_tactics]
test12 [lemma, in AreaMethod.bench_normalization_tactics]
test13 [lemma, in AreaMethod.bench_normalization_tactics]
test15 [lemma, in AreaMethod.bench_normalization_tactics]
test16 [lemma, in AreaMethod.bench_normalization_tactics]
test172 [lemma, in AreaMethod.bench_normalization_tactics]
test173 [lemma, in AreaMethod.bench_normalization_tactics]
test174 [lemma, in AreaMethod.bench_normalization_tactics]
test18 [lemma, in AreaMethod.bench_normalization_tactics]
test19 [lemma, in AreaMethod.bench_normalization_tactics]
test2 [lemma, in AreaMethod.bench_normalization_tactics]
test20 [lemma, in AreaMethod.bench_normalization_tactics]
test21 [lemma, in AreaMethod.bench_normalization_tactics]
test22 [lemma, in AreaMethod.bench_normalization_tactics]
test23 [lemma, in AreaMethod.bench_normalization_tactics]
test24 [lemma, in AreaMethod.bench_normalization_tactics]
test25 [lemma, in AreaMethod.bench_normalization_tactics]
test26 [lemma, in AreaMethod.bench_normalization_tactics]
test27 [lemma, in AreaMethod.bench_normalization_tactics]
test28 [lemma, in AreaMethod.bench_normalization_tactics]
test29 [lemma, in AreaMethod.bench_normalization_tactics]
test3 [lemma, in AreaMethod.bench_normalization_tactics]
test30 [lemma, in AreaMethod.bench_normalization_tactics]
test31 [lemma, in AreaMethod.bench_normalization_tactics]
test32 [lemma, in AreaMethod.bench_normalization_tactics]
test35 [lemma, in AreaMethod.bench_normalization_tactics]
test36 [lemma, in AreaMethod.bench_normalization_tactics]
test4 [lemma, in AreaMethod.bench_normalization_tactics]
test40 [lemma, in AreaMethod.bench_normalization_tactics]
test41 [lemma, in AreaMethod.bench_normalization_tactics]
test42 [lemma, in AreaMethod.bench_normalization_tactics]
test43 [lemma, in AreaMethod.bench_normalization_tactics]
test44 [lemma, in AreaMethod.bench_normalization_tactics]
test45 [lemma, in AreaMethod.bench_normalization_tactics]
test46 [lemma, in AreaMethod.bench_normalization_tactics]
test47 [lemma, in AreaMethod.bench_normalization_tactics]
test48 [lemma, in AreaMethod.bench_normalization_tactics]
test49 [lemma, in AreaMethod.bench_normalization_tactics]
test5 [lemma, in AreaMethod.bench_normalization_tactics]
test50 [lemma, in AreaMethod.bench_normalization_tactics]
test51 [lemma, in AreaMethod.bench_normalization_tactics]
test52 [lemma, in AreaMethod.bench_normalization_tactics]
test53 [lemma, in AreaMethod.bench_normalization_tactics]
test54 [lemma, in AreaMethod.bench_normalization_tactics]
test55 [lemma, in AreaMethod.bench_normalization_tactics]
test56 [lemma, in AreaMethod.bench_normalization_tactics]
test57 [lemma, in AreaMethod.bench_normalization_tactics]
test58 [lemma, in AreaMethod.bench_normalization_tactics]
test59 [lemma, in AreaMethod.bench_normalization_tactics]
test6 [lemma, in AreaMethod.bench_normalization_tactics]
test60 [lemma, in AreaMethod.bench_normalization_tactics]
test61 [lemma, in AreaMethod.bench_normalization_tactics]
test62 [lemma, in AreaMethod.bench_normalization_tactics]
test65 [lemma, in AreaMethod.bench_normalization_tactics]
test7 [lemma, in AreaMethod.bench_normalization_tactics]
test8 [lemma, in AreaMethod.bench_normalization_tactics]
test9 [lemma, in AreaMethod.bench_normalization_tactics]
thales [lemma, in AreaMethod.advanced_parallel_lemmas]
thales_2 [lemma, in AreaMethod.advanced_parallel_lemmas]
th2_41 [lemma, in AreaMethod.examples_2]
th6_259 [lemma, in AreaMethod.examples_6]
th6_41_b [lemma, in AreaMethod.examples_3]
th6_257 [lemma, in AreaMethod.examples_2]
th6_258 [lemma, in AreaMethod.examples_3]
th6_239 [lemma, in AreaMethod.examples_3]
th6_256_1 [lemma, in AreaMethod.examples_2]
th6_232 [lemma, in AreaMethod.examples_3]
th6_43 [lemma, in AreaMethod.examples_2]
th6_40_Centroid [lemma, in AreaMethod.examples_2]
th6_42 [lemma, in AreaMethod.examples_2]
th6_7 [lemma, in AreaMethod.examples_2]
th6_234_1 [lemma, in AreaMethod.examples_3]
th6_41 [lemma, in AreaMethod.examples_3]
th6_6 [lemma, in AreaMethod.examples_2]
trivial_col2 [lemma, in AreaMethod.geometry_tools_lemmas]
trivial_col1 [lemma, in AreaMethod.geometry_tools_lemmas]
trivial_col3 [lemma, in AreaMethod.geometry_tools_lemmas]
two_sides_par_eq_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]


U

uniformize_areas_formula2_correct [lemma, in AreaMethod.Rgeometry_tools]
uniformize_areas_formula2 [definition, in AreaMethod.Rgeometry_tools]
uniformize_areas_correct [lemma, in AreaMethod.Rgeometry_tools]
uniformize_areas_formula2_correct_gen [lemma, in AreaMethod.Rgeometry_tools]
uniformize_areas [definition, in AreaMethod.Rgeometry_tools]


W

weak_parallelogram_weak_3_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram [definition, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_3 [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_parallelogram_weak_2_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_4 [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_2 [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_2_parallelogram [definition, in AreaMethod.advanced_parallel_lemmas]
weak_2_parallelogram_weak_3_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_1 [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_para_1 [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_parallelogram_parallelogram [lemma, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_eq_side [lemma, in AreaMethod.pythagoras_difference_lemmas]
weak_parallelogram [definition, in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_parallel [lemma, in AreaMethod.pythagoras_difference_lemmas]


Z

zeroegal [lemma, in AreaMethod.geometry_tools_lemmas]


other

_ + _ (F_scope) [notation, in AreaMethod.field]
_ - _ (F_scope) [notation, in AreaMethod.field]
_ ** _ (F_scope) [notation, in AreaMethod.chou_gao_zhang_axioms]
/ _ (F_scope) [notation, in AreaMethod.field]
1 (F_scope) [notation, in AreaMethod.field]
- _ (F_scope) [notation, in AreaMethod.field]
2 (F_scope) [notation, in AreaMethod.field]
_ * _ (F_scope) [notation, in AreaMethod.field]
_ / _ (F_scope) [notation, in AreaMethod.field]
0 (F_scope) [notation, in AreaMethod.field]



Lemma Index

A

aux [in AreaMethod.freepoints]
aux_co_side_4 [in AreaMethod.ratios_elimination_lemmas]
aux_co_side_2 [in AreaMethod.ratios_elimination_lemmas]
aux_co_side_1 [in AreaMethod.ratios_elimination_lemmas]
aux_co_side_3 [in AreaMethod.ratios_elimination_lemmas]
A1a [in AreaMethod.geometry_tools_lemmas]
A2bgen [in AreaMethod.basic_geometric_facts]
A6_6 [in AreaMethod.basic_geometric_facts]
A6_5 [in AreaMethod.basic_geometric_facts]
A6_2 [in AreaMethod.basic_geometric_facts]
A6_4 [in AreaMethod.basic_geometric_facts]
A6_3 [in AreaMethod.basic_geometric_facts]
A6_1 [in AreaMethod.basic_geometric_facts]


B

build_point_not_collinear_1 [in AreaMethod.basic_geometric_facts]
build_point_not_collinear_2 [in AreaMethod.basic_geometric_facts]


C

centroid_midpoint_centroid_2 [in AreaMethod.examples_centroid]
centroid_check [in AreaMethod.examples_centroid]
centroid_midpoint_centroid [in AreaMethod.examples_centroid]
Ceva [in AreaMethod.examples_2]
check_co_circle [in AreaMethod.euclidean_constructions]
check_circumcenter [in AreaMethod.examples_circumcenter]
circle_square_triangle [in AreaMethod.examples_6]
col_4 [in AreaMethod.basic_geometric_facts]
col_par_4 [in AreaMethod.parallel_lemmas]
col_par_2 [in AreaMethod.parallel_lemmas]
col_2 [in AreaMethod.basic_geometric_facts]
col_par_par [in AreaMethod.parallel_lemmas]
col_decS [in AreaMethod.elimination_prepare]
col_not_col_1 [in AreaMethod.basic_geometric_facts]
col_5 [in AreaMethod.basic_geometric_facts]
col_par_3 [in AreaMethod.parallel_lemmas]
col_pyth [in AreaMethod.pythagoras_difference]
col_3 [in AreaMethod.basic_geometric_facts]
col_1 [in AreaMethod.basic_geometric_facts]
col_trans_1 [in AreaMethod.basic_geometric_facts]
col_dec [in AreaMethod.chou_gao_zhang_axioms]
col_par_1 [in AreaMethod.parallel_lemmas]
combine_inter_parallel [in AreaMethod.simplify_constructions]
common_point_not_par_aux [in AreaMethod.parallel_lemmas]
common_point_not_par [in AreaMethod.parallel_lemmas]
Conversemenelaus [in AreaMethod.examples_2]
ConverseMenelauseQuadri [in AreaMethod.examples_2]
co_side_bis [in AreaMethod.basic_geometric_facts]
co_side [in AreaMethod.basic_geometric_facts]
co_side_main [in AreaMethod.basic_geometric_facts]
co_side_elim_3 [in AreaMethod.ratios_elimination_lemmas]
co_side_elim_2 [in AreaMethod.ratios_elimination_lemmas]
co_side_ter [in AreaMethod.basic_geometric_facts]
co_side_elim_4 [in AreaMethod.ratios_elimination_lemmas]
co_side_elim_1 [in AreaMethod.ratios_elimination_lemmas]


D

degenerated_ratio [in AreaMethod.geometry_tools_lemmas]
Desargues [in AreaMethod.examples_2]
diago_par_intersect [in AreaMethod.parallel_lemmas]
diag_mid_point_parallel [in AreaMethod.basic_geometric_facts]
diff_not_col_par_not_col [in AreaMethod.advanced_parallel_lemmas]
dirseg_simpl_1 [in AreaMethod.basic_geometric_facts]
dirseg_2 [in AreaMethod.basic_geometric_facts]
dirseg_3 [in AreaMethod.basic_geometric_facts]
dirseg_1 [in AreaMethod.basic_geometric_facts]
dirseg_simpl_2 [in AreaMethod.basic_geometric_facts]
dirseg_4 [in AreaMethod.basic_geometric_facts]
dirsur_1 [in AreaMethod.basic_geometric_facts]
divnonzero [in AreaMethod.field_general_properties]


E

egalcol [in AreaMethod.basic_geometric_facts]
egalzero [in AreaMethod.geometry_tools_lemmas]
elim_py_inter_ll_right_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_left_right_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_on_line_middle [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_spec_a [in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_left_right_invariant [in AreaMethod.py_elimination_lemmas]
elim_length_ratio_inter_ll_2 [in AreaMethod.ratios_elimination_lemmas]
elim_py_midpoint_left_right [in AreaMethod.py_elimination_lemmas]
elim_py_on_perp_d_middle [in AreaMethod.py_elimination_lemmas]
elim_py_on_line_right [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_b [in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_right [in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_inter_line_parallel_1 [in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_spec_a [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_b [in AreaMethod.py_elimination_lemmas]
elim_py_a_ratio_middle [in AreaMethod.area_coords_elimination]
elim_length_ratio_on_line_d_1 [in AreaMethod.ratios_elimination_lemmas]
elim_py_on_parallel_d_middle [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_a [in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_right [in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_middle_invariant [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_a [in AreaMethod.py_elimination_lemmas]
elim_signed_area_a_ratio [in AreaMethod.area_coords_elimination]
elim_ratio_on_perp_d_spec_b [in AreaMethod.py_elimination_lemmas]
elim_area_on_foot_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_left_right [in AreaMethod.py_elimination_lemmas]
elim_area_on_foot [in AreaMethod.py_elimination_lemmas]
elim_py_on_perp_d_left_right [in AreaMethod.py_elimination_lemmas]
elim_py_inter_ll_middle [in AreaMethod.py_elimination_lemmas]
elim_area_on_line_d [in AreaMethod.area_elimination_lemmas]
elim_area_on_inter_parallel_parallel_RY [in AreaMethod.ratios_elimination_lemmas]
elim_py_on_foot_middle [in AreaMethod.py_elimination_lemmas]
elim_area_on_parallel [in AreaMethod.area_elimination_lemmas]
elim_area_inter_ll [in AreaMethod.area_elimination_lemmas]
elim_length_ratio_on_inter_parallel_parallel_2 [in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_a_aux [in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_line_2 [in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_foot_a_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_on_parallel_d_right [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_a_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_on_foot_right_invariant [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_spec_b [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_perp_d_b_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_on_line_d_middle [in AreaMethod.py_elimination_lemmas]
elim_area_on_inter_parallel_parallel [in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_line_1 [in AreaMethod.ratios_elimination_lemmas]
elim_area_on_perp_d [in AreaMethod.py_elimination_lemmas]
elim_py_on_perp_d_right [in AreaMethod.py_elimination_lemmas]
elim_py_on_line_d_right [in AreaMethod.py_elimination_lemmas]
elim_length_ratio_inter_ll_1_spec [in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_parallel_d_1 [in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_b_aux [in AreaMethod.py_elimination_lemmas]
elim_area_on_parallel_d [in AreaMethod.area_elimination_lemmas]
elim_py_inter_ll_middle_invariant [in AreaMethod.py_elimination_lemmas]
elim_py_on_line_d_left_right [in AreaMethod.py_elimination_lemmas]
elim_py_a_ratio_right [in AreaMethod.area_coords_elimination]
elim_area_on_line [in AreaMethod.area_elimination_lemmas]
elim_length_ratio_inter_ll_1 [in AreaMethod.ratios_elimination_lemmas]
elim_py_on_parallel_d_left_right [in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_line_d_2 [in AreaMethod.ratios_elimination_lemmas]
elim_ratio_on_perp_d_b_auxi [in AreaMethod.py_elimination_lemmas]
elim_length_ratio_on_parallel_d_2 [in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_inter_ll_2_spec [in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_inter_parallel_parallel_1 [in AreaMethod.ratios_elimination_lemmas]
elim_length_ratio_on_inter_line_parallel_2 [in AreaMethod.ratios_elimination_lemmas]
elim_py_on_foot_left_right [in AreaMethod.py_elimination_lemmas]
elim_ratio_on_foot_b_invariant [in AreaMethod.py_elimination_lemmas]
elim_area_on_inter_line_parallel [in AreaMethod.area_elimination_lemmas]
elim_py_a_ratio_left_right [in AreaMethod.area_coords_elimination]
eq_simpl_7 [in AreaMethod.area_method]
eq_simpl_3 [in AreaMethod.area_method]
eq_simpl_6 [in AreaMethod.area_method]
eq_simpl_2 [in AreaMethod.area_method]
eq_simpl_1 [in AreaMethod.area_method]
eq_dec_points [in AreaMethod.chou_gao_zhang_axioms]
eq_simpl [in AreaMethod.my_field_tac]
eq_simpl_10 [in AreaMethod.area_method]
eq_simpl_9 [in AreaMethod.area_method]
eq_simpl_5 [in AreaMethod.area_method]
eq_simpl_8 [in AreaMethod.area_method]
eq_simpl_4 [in AreaMethod.area_method]
eq_half_eq_zero [in AreaMethod.pythagoras_difference_lemmas]
eq_diff_diff [in AreaMethod.basic_geometric_facts]
essai [in AreaMethod.tests_elimination_tactics_py]
euclid_parallel_existence_strong [in AreaMethod.basic_geometric_facts]
euclid_parallel_existence [in AreaMethod.basic_geometric_facts]
euler_line [in AreaMethod.examples_centroid]
example_construction_simplification [in AreaMethod.examples_1]
example6_9 [in AreaMethod.examples_3]
exercice2_38_3 [in AreaMethod.examples_3]
Exo55Hartsshorne [in AreaMethod.examples_2]
ex1_6auto [in AreaMethod.examples_2]


F

field_prop_5 [in AreaMethod.field_general_properties]
field_prop_3 [in AreaMethod.field_general_properties]
field_prop_1 [in AreaMethod.field_general_properties]
field_prop_2 [in AreaMethod.geometry_tools_lemmas]
field_prop_4 [in AreaMethod.field_general_properties]
field_prop1 [in AreaMethod.basic_geometric_facts]
Fmult_Fplus_distr_r [in AreaMethod.field]
freepoint_elimination_aux [in AreaMethod.freepoints]
free_points_ratio_elimination_7 [in AreaMethod.freepoints]
free_points_ratio_elimination_3 [in AreaMethod.freepoints]
free_points_ratio_elimination_5 [in AreaMethod.freepoints]
free_points_ratio_elimination_7_non_zero_denom [in AreaMethod.freepoints]
free_points_area_elimination [in AreaMethod.freepoints]
free_points_ratio_elimination_6_non_zero_denom [in AreaMethod.freepoints]
free_point_ratio_elimination_2 [in AreaMethod.freepoints]
free_points_ratio_elimination_6 [in AreaMethod.freepoints]
free_points_ratio_elimination_1 [in AreaMethod.freepoints]
free_points_ratio_elimination_8 [in AreaMethod.freepoints]
free_points_ratio_elimination_4 [in AreaMethod.freepoints]
FRth [in AreaMethod.field]
Fth [in AreaMethod.field]
f_equal2_sym [in AreaMethod.area_method]


G

gauss_line [in AreaMethod.examples_2]


H

half [in AreaMethod.geometry_tools]
herron_qin [in AreaMethod.pythagoras_difference_lemmas]


I

inter_ll_comm4 [in AreaMethod.ratios_elimination_lemmas]
inter_llex [in AreaMethod.construction_lemmas]
inter_ll_comm1 [in AreaMethod.ratios_elimination_lemmas]
inter_ll_ex [in AreaMethod.construction_lemmas]
inter_ll_comm2 [in AreaMethod.ratios_elimination_lemmas]
inter_ll_comm3 [in AreaMethod.ratios_elimination_lemmas]
inter_unicity_2 [in AreaMethod.basic_geometric_facts]
inter_unicity [in AreaMethod.basic_geometric_facts]
invariant_par_on_line_d_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_d_1_length_ratio_2 [in AreaMethod.ratios_elimination_lemmas]
invariant_div_3 [in AreaMethod.my_field_tac]
invariant_par_on_parallel_d_1_length_ratio_2 [in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_d_1_length_ratio_3 [in AreaMethod.ratios_elimination_lemmas]
invariant_inverse_ratio [in AreaMethod.elimination_prepare]
invariant_par_on_line_1_length_ratio_3 [in AreaMethod.ratios_elimination_lemmas]
invariant_par_on_line_1_length_ratio_2 [in AreaMethod.ratios_elimination_lemmas]
invariant_div_1 [in AreaMethod.my_field_tac]
invariant_par_on_parallel_d_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
inverse_ratio [in AreaMethod.field_general_properties]
is_orthocenter_non_zero' [in AreaMethod.area_coords_constructions]
is_circumcenter_non_zero [in AreaMethod.area_coords_constructions]
is_orthocenter_equiv [in AreaMethod.area_coords_constructions]
is_circumcenter_non_zero' [in AreaMethod.area_coords_constructions]
is_orthocenter_non_zero [in AreaMethod.area_coords_constructions]
is_midpoint_A [in AreaMethod.examples_2]
is_circumcenter_equiv [in AreaMethod.area_coords_constructions]


L

lambda_zero_on_parallel_d [in AreaMethod.ratios_elimination_lemmas]
Lc [in AreaMethod.field_variable_isolation_tactic]
Lcdiv1 [in AreaMethod.field_variable_isolation_tactic]
Lcdiv2 [in AreaMethod.field_variable_isolation_tactic]
Lcinv [in AreaMethod.field_variable_isolation_tactic]
Lcmult1 [in AreaMethod.field_variable_isolation_tactic]
Lcmult2 [in AreaMethod.field_variable_isolation_tactic]
Lcm1 [in AreaMethod.field_variable_isolation_tactic]
Lcm2 [in AreaMethod.field_variable_isolation_tactic]
Lcop1 [in AreaMethod.field_variable_isolation_tactic]
Lcp1 [in AreaMethod.field_variable_isolation_tactic]
Lcp2 [in AreaMethod.field_variable_isolation_tactic]
ldiff [in AreaMethod.geometry_tools_lemmas]
lpar1 [in AreaMethod.geometry_tools_lemmas]
lpar2 [in AreaMethod.geometry_tools_lemmas]
lpar3 [in AreaMethod.geometry_tools_lemmas]
l_27_b [in AreaMethod.pythagoras_difference_lemmas]
l_3_4 [in AreaMethod.pythagoras_difference_lemmas]
l_3_40 [in AreaMethod.examples_6]
l_6_271 [in AreaMethod.examples_6]
l_25_c [in AreaMethod.pythagoras_difference_lemmas]
l_6_295 [in AreaMethod.examples_interactive]
l_28_a [in AreaMethod.pythagoras_difference_lemmas]
l_3_4_b [in AreaMethod.pythagoras_difference_lemmas]
l_24_c_on_foot [in AreaMethod.pythagoras_difference_lemmas]
l_25_a [in AreaMethod.pythagoras_difference_lemmas]
l_6_268 [in AreaMethod.examples_6]
l_6_267 [in AreaMethod.examples_6]
l_6_264 [in AreaMethod.examples_6]
l_6_273 [in AreaMethod.examples_interactive]
l_6_266 [in AreaMethod.examples_6]
l_6_134 [in AreaMethod.examples_6]
l_6_272 [in AreaMethod.examples_6]
l_6_269 [in AreaMethod.examples_6]
l_3_41 [in AreaMethod.examples_6]
l_6_270 [in AreaMethod.examples_6]
l_28_b [in AreaMethod.pythagoras_difference_lemmas]
l_27_a [in AreaMethod.pythagoras_difference_lemmas]
l_6_265 [in AreaMethod.examples_6]
l_6_191 [in AreaMethod.examples_interactive]
l_28_midpoint [in AreaMethod.pythagoras_difference_lemmas]
l_24_a [in AreaMethod.pythagoras_difference_lemmas]
l_28_b_midpoint [in AreaMethod.pythagoras_difference_lemmas]
l_24_c [in AreaMethod.pythagoras_difference_lemmas]
l_25_b [in AreaMethod.pythagoras_difference_lemmas]
l_27_c [in AreaMethod.pythagoras_difference_lemmas]
l_24_b [in AreaMethod.pythagoras_difference_lemmas]
l_3_45 [in AreaMethod.examples_6]
l1_24 [in AreaMethod.parallel_lemmas]
l1_25_aux [in AreaMethod.advanced_parallel_lemmas]
l1_25 [in AreaMethod.advanced_parallel_lemmas]
l2_11a [in AreaMethod.advanced_parallel_lemmas]
l2_12b [in AreaMethod.advanced_parallel_lemmas]
l2_11a_strong [in AreaMethod.advanced_parallel_lemmas]
l2_11b_strong_strong [in AreaMethod.advanced_parallel_lemmas]
l2_9 [in AreaMethod.basic_geometric_facts]
l2_11b_strong_strong_strong [in AreaMethod.advanced_parallel_lemmas]
l2_11b [in AreaMethod.advanced_parallel_lemmas]
l2_12b_strong_3 [in AreaMethod.advanced_parallel_lemmas]
l2_12a [in AreaMethod.advanced_parallel_lemmas]
l2_9aux [in AreaMethod.basic_geometric_facts]
l2_15 [in AreaMethod.advanced_parallel_lemmas]
l2_11a_strong_strong [in AreaMethod.advanced_parallel_lemmas]
l2_7 [in AreaMethod.basic_geometric_facts]
l2_11a_strong_strong_strong [in AreaMethod.advanced_parallel_lemmas]
l2_12a_strong_3 [in AreaMethod.advanced_parallel_lemmas]
l2_9_weak [in AreaMethod.basic_geometric_facts]
l2_11a_strong_strong_strong_aux [in AreaMethod.advanced_parallel_lemmas]
l3_6_b [in AreaMethod.pythagoras_difference_lemmas]
l3_8_a [in AreaMethod.pythagoras_difference_lemmas]
l3_6 [in AreaMethod.pythagoras_difference_lemmas]
l3_43 [in AreaMethod.examples_2]
l3_44 [in AreaMethod.examples_3]
l3_10 [in AreaMethod.pythagoras_difference_lemmas]
l3_8_b [in AreaMethod.pythagoras_difference_lemmas]
l3_9 [in AreaMethod.pythagoras_difference_lemmas]
l3_10b [in AreaMethod.pythagoras_difference_lemmas]
l3_5_py [in AreaMethod.pythagoras_difference_lemmas]
l3_51 [in AreaMethod.examples_6]
l3_9_aux [in AreaMethod.pythagoras_difference_lemmas]
l6_44 [in AreaMethod.examples_6]
l6_47 [in AreaMethod.examples_centroid]
l6_196 [in AreaMethod.examples_circumcenter]
l6_86 [in AreaMethod.examples_circumcenter]
l6_90 [in AreaMethod.examples_circumcenter]
l6_224 [in AreaMethod.examples_5]
l6_217 [in AreaMethod.examples_2]
l6_46 [in AreaMethod.examples_6]
l6_17 [in AreaMethod.examples_5]
l6_144 [in AreaMethod.examples_interactive]
l6_52 [in AreaMethod.examples_5]
l6_69 [in AreaMethod.examples_5]
l6_56 [in AreaMethod.examples_5]
l6_17 [in AreaMethod.examples_6]
l6_95 [in AreaMethod.examples_circumcenter]
l6_44 [in AreaMethod.examples_centroid]
l6_84 [in AreaMethod.examples_6]
l6_88 [in AreaMethod.examples_circumcenter]
l6_87 [in AreaMethod.examples_circumcenter]
l6_223 [in AreaMethod.examples_5]
l6_63 [in AreaMethod.examples_interactive]
l6_67 [in AreaMethod.examples_5]
l6_15 [in AreaMethod.examples_interactive]
l6_55 [in AreaMethod.examples_5]
l6_197 [in AreaMethod.examples_5]
l6_222 [in AreaMethod.examples_6]
l6_218 [in AreaMethod.examples_5]


M

Menelaus [in AreaMethod.examples_2]
MenelausQuadri [in AreaMethod.examples_2]
midpoint_ratio_1 [in AreaMethod.pythagoras_difference_lemmas]
midpoint_elim [in AreaMethod.examples_interactive]
midpoint_on_line_d [in AreaMethod.pythagoras_difference_lemmas]
midpoint_is_midpoint [in AreaMethod.pythagoras_difference_lemmas]
midpoint_ratio_2 [in AreaMethod.pythagoras_difference_lemmas]
mid_point_degenerated_1 [in AreaMethod.basic_geometric_facts]
mid_point_ex [in AreaMethod.basic_geometric_facts]
mid_point_comm [in AreaMethod.basic_geometric_facts]
mid_point_equation [in AreaMethod.parallel_lemmas]
mid_point_degenerated_2 [in AreaMethod.basic_geometric_facts]
mid_point_degenerated_3 [in AreaMethod.basic_geometric_facts]
multnonzero [in AreaMethod.field_general_properties]
multnonzero_r [in AreaMethod.field_general_properties]
multnonzero_l [in AreaMethod.field_general_properties]


N

nateq_prop [in AreaMethod.Rgeometry_tools]
neq_not_zero [in AreaMethod.geometry_tools_lemmas]
nine_point_1 [in AreaMethod.examples_6]
nonzerodiv [in AreaMethod.field_general_properties]
nonzeroinv [in AreaMethod.field_general_properties]
nonzeromult [in AreaMethod.field_general_properties]
non_zero_denom_on_inter_parallel_parallel_area [in AreaMethod.area_elimination_lemmas]
non_zero_denom_on_line_2_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_d_2_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_inter_line_parallel_area [in AreaMethod.area_elimination_lemmas]
non_zero_denom_on_parallel_d_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_d_1_length_ratio_seg [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_area [in AreaMethod.area_elimination_lemmas]
non_zero_denom_on_line_1_length_ratio_seg [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_parallel_d_area [in AreaMethod.area_elimination_lemmas]
non_zero_denom_inter_ll_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_parallel_d_2_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_inter_ll_2_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_on_line_d_1_length_ratio [in AreaMethod.ratios_elimination_lemmas]
non_zero_denom_inter_ll_area [in AreaMethod.area_elimination_lemmas]
notcolnotegal_2 [in AreaMethod.basic_geometric_facts]
notcolnotegal_1 [in AreaMethod.basic_geometric_facts]
notcolnotegal_3 [in AreaMethod.basic_geometric_facts]
noteqnotzero [in AreaMethod.basic_geometric_facts]
notparallelnotegal_1 [in AreaMethod.basic_geometric_facts]
notparallelnotegal_2 [in AreaMethod.basic_geometric_facts]
not_para_eq_4 [in AreaMethod.parallel_lemmas]
not_eq_py_not_zero [in AreaMethod.pythagoras_difference]
not_para_eq_2 [in AreaMethod.parallel_lemmas]
not_parallel_not_eq_1 [in AreaMethod.basic_geometric_facts]
not_para_eq_3 [in AreaMethod.parallel_lemmas]
not_para_eq_1 [in AreaMethod.parallel_lemmas]
not_parallel_not_eq_2 [in AreaMethod.basic_geometric_facts]
not_para_eq_5 [in AreaMethod.parallel_lemmas]
not_perp_to_itself [in AreaMethod.pythagoras_difference_lemmas]
not_para_eq_6 [in AreaMethod.parallel_lemmas]
nuldirseg [in AreaMethod.geometry_tools_lemmas]
number_dec [in AreaMethod.chou_gao_zhang_axioms]


O

on_inter_parallel_parallel_ex [in AreaMethod.construction_lemmas_2]
on_line_dex_spec [in AreaMethod.advanced_parallel_lemmas]
on_line_dex_spec_strong_f [in AreaMethod.advanced_parallel_lemmas]
on_foot_per [in AreaMethod.pythagoras_difference_lemmas]
on_line_dex_spec_strong_bis [in AreaMethod.advanced_parallel_lemmas]
on_line_to_on_line_d [in AreaMethod.construction_lemmas]
on_line_dex_spec_strong_ter [in AreaMethod.advanced_parallel_lemmas]
on_parallel_d_ex [in AreaMethod.construction_lemmas]
on_parallelex [in AreaMethod.construction_lemmas]
on_parallel_ex [in AreaMethod.construction_lemmas]
on_perp_d_ex [in AreaMethod.euclidean_constructions_2]
on_line_dex [in AreaMethod.construction_lemmas]
on_perp_to_on_perp_d [in AreaMethod.euclidean_constructions]
on_foot_area_paper [in AreaMethod.pythagoras_difference]
on_line_dex_spec_strong [in AreaMethod.advanced_parallel_lemmas]
on_inter_line_parallel_ex [in AreaMethod.construction_lemmas_2]
on_line_ex [in AreaMethod.construction_lemmas]
on_line_iff_on_parallel [in AreaMethod.euclidean_constructions]
on_lineex [in AreaMethod.construction_lemmas]
on_parallel_to_on_parallel_d [in AreaMethod.construction_lemmas]
on_inter_parallel_parallel_ex_aux [in AreaMethod.construction_lemmas_2]
on_line_d_iff_on_parallel_d [in AreaMethod.euclidean_constructions]
opzero [in AreaMethod.field_general_properties]


P

Pappus [in AreaMethod.examples_4]
Pappus_2 [in AreaMethod.examples_4]
parallellogram_construction_2 [in AreaMethod.examples_1]
parallellogram_construction [in AreaMethod.examples_1]
parallellogram_second_parallel [in AreaMethod.examples_1]
parallelogram_weak_3_parallelogram [in AreaMethod.advanced_parallel_lemmas]
parallelogram_weak_parallelogram [in AreaMethod.advanced_parallel_lemmas]
parallelogram_midpoint [in AreaMethod.examples_1]
parallel_equiv [in AreaMethod.area_method]
parallel_not_perp [in AreaMethod.pythagoras_difference_lemmas]
parallel_dec [in AreaMethod.chou_gao_zhang_axioms]
parallel_transitivity [in AreaMethod.examples_1]
parallel_transitivity [in AreaMethod.area_elimination_lemmas]
parallel_side_eq_weak_para [in AreaMethod.advanced_parallel_lemmas]
parallel_side_eq_weak_weak_para [in AreaMethod.advanced_parallel_lemmas]
parallel_side_eq_weak_weak_weak_para [in AreaMethod.advanced_parallel_lemmas]
parallel_side_eq_parallel' [in AreaMethod.basic_geometric_facts]
parallel_dec [in AreaMethod.freepoints]
parallel_pseudo_transitivity [in AreaMethod.examples_1]
para_1 [in AreaMethod.parallel_lemmas]
para_not_col_1 [in AreaMethod.parallel_lemmas]
para_not_eq_4 [in AreaMethod.parallel_lemmas]
para_not_eq_3 [in AreaMethod.parallel_lemmas]
para_not_col_3 [in AreaMethod.parallel_lemmas]
para_4 [in AreaMethod.parallel_lemmas]
para_2 [in AreaMethod.parallel_lemmas]
para_not_eq_6 [in AreaMethod.parallel_lemmas]
para_not_eq_5 [in AreaMethod.parallel_lemmas]
para_not_col_2 [in AreaMethod.parallel_lemmas]
para_not_eq_2 [in AreaMethod.parallel_lemmas]
para_not_eq_1 [in AreaMethod.parallel_lemmas]
para_3 [in AreaMethod.parallel_lemmas]
par_col_col_1 [in AreaMethod.parallel_lemmas]
par_not_all_col [in AreaMethod.basic_geometric_facts]
par_2 [in AreaMethod.basic_geometric_facts]
par_col_col_2 [in AreaMethod.parallel_lemmas]
par_1 [in AreaMethod.basic_geometric_facts]
par_col_col_4 [in AreaMethod.parallel_lemmas]
par_col_col_3 [in AreaMethod.parallel_lemmas]
par_aux_1 [in AreaMethod.basic_geometric_facts]
Pascal [in AreaMethod.examples_2]
pascalian_ax [in AreaMethod.advanced_parallel_lemmas]
perp_9 [in AreaMethod.pythagoras_difference]
perp_bissect_perp [in AreaMethod.examples_6]
perp_bissect_eq_distance [in AreaMethod.examples_6]
perp_1 [in AreaMethod.pythagoras_difference]
perp_4 [in AreaMethod.pythagoras_difference]
perp_not_eq_not_perp [in AreaMethod.pythagoras_difference_lemmas]
perp_8 [in AreaMethod.pythagoras_difference]
perp_col_perp [in AreaMethod.pythagoras_difference_lemmas]
perp_6 [in AreaMethod.pythagoras_difference]
perp_3 [in AreaMethod.pythagoras_difference]
perp_5 [in AreaMethod.pythagoras_difference]
perp_2 [in AreaMethod.pythagoras_difference]
perp_bissect_eq_angle [in AreaMethod.examples_6]
perp_7 [in AreaMethod.pythagoras_difference]
perp_not_parallel [in AreaMethod.pythagoras_difference_lemmas]
perp4_perp [in AreaMethod.pythagoras_difference_lemmas]
per_dec [in AreaMethod.pythagoras_difference_lemmas]
per_col_eq [in AreaMethod.pythagoras_difference_lemmas]
per_area [in AreaMethod.pythagoras_difference_lemmas]
proj_ex [in AreaMethod.euclidean_constructions]
Prop51Hartsshorne [in AreaMethod.examples_2]
Prop51Hartsshornebis [in AreaMethod.examples_1]
Prop51Hartsshornebis [in AreaMethod.examples_2]
Prop54Hartsshorne [in AreaMethod.examples_2]
pyth_sym [in AreaMethod.pythagoras_difference]
pyth_simpl_4 [in AreaMethod.pythagoras_difference]
pyth_simpl_3 [in AreaMethod.pythagoras_difference]
pyth_simpl_1 [in AreaMethod.pythagoras_difference]
pyth_simpl_2 [in AreaMethod.pythagoras_difference]
py_zero_eq [in AreaMethod.pythagoras_difference]
py4_6 [in AreaMethod.pythagoras_difference]
py4_3 [in AreaMethod.pythagoras_difference]
py4_simpl_4 [in AreaMethod.pythagoras_difference]
py4_7 [in AreaMethod.pythagoras_difference]
py4_simpl_2 [in AreaMethod.pythagoras_difference]
py4_simpl_3 [in AreaMethod.pythagoras_difference]
py4_4 [in AreaMethod.pythagoras_difference]
py4_simpl_5 [in AreaMethod.pythagoras_difference]
py4_1 [in AreaMethod.pythagoras_difference]
py4_5 [in AreaMethod.pythagoras_difference]
py4_simpl_6 [in AreaMethod.pythagoras_difference]
py4_2 [in AreaMethod.pythagoras_difference]
py4_simpl_1 [in AreaMethod.pythagoras_difference]


R

rectangle_1 [in AreaMethod.examples_6]
rectangle_3 [in AreaMethod.examples_6]
rectangle_2 [in AreaMethod.examples_6]
remove_opp [in AreaMethod.my_field_tac]
remove_inv [in AreaMethod.my_field_tac]


S

same_denom_div_2 [in AreaMethod.my_field_tac]
same_denom_mul_2 [in AreaMethod.my_field_tac]
same_denom_min_2 [in AreaMethod.my_field_tac]
same_denom_add_3 [in AreaMethod.my_field_tac]
same_denom_add_2 [in AreaMethod.my_field_tac]
same_denom_conclude_2 [in AreaMethod.my_field_tac]
same_denom_min_1 [in AreaMethod.my_field_tac]
same_denom_add_1 [in AreaMethod.my_field_tac]
same_denom_conclude_4 [in AreaMethod.my_field_tac]
same_denom_div_1 [in AreaMethod.my_field_tac]
same_denom_mul_3 [in AreaMethod.my_field_tac]
same_denom_conclude_5 [in AreaMethod.my_field_tac]
same_denom_mul_1 [in AreaMethod.my_field_tac]
same_denom_conclude_3 [in AreaMethod.my_field_tac]
same_denom_div_3 [in AreaMethod.my_field_tac]
same_denom_conclude_1 [in AreaMethod.my_field_tac]
same_denom_min_3 [in AreaMethod.my_field_tac]
simplif_correct [in AreaMethod.Rgeometry_tools]
simplring1 [in AreaMethod.geometry_tools_lemmas]
simp_frac_4 [in AreaMethod.my_field_tac]
simp_9 [in AreaMethod.my_field_tac]
simp_frac_5 [in AreaMethod.my_field_tac]
simp_frac_9 [in AreaMethod.my_field_tac]
simp_frac_7 [in AreaMethod.my_field_tac]
simp_frac_10 [in AreaMethod.my_field_tac]
simp_frac_6 [in AreaMethod.my_field_tac]
simp_2 [in AreaMethod.my_field_tac]
simp_7 [in AreaMethod.my_field_tac]
simp_frac_2 [in AreaMethod.my_field_tac]
simp_5 [in AreaMethod.my_field_tac]
simp_frac_16 [in AreaMethod.my_field_tac]
simp_frac_15 [in AreaMethod.my_field_tac]
simp_4 [in AreaMethod.my_field_tac]
simp_13 [in AreaMethod.my_field_tac]
simp_frac_16_inv [in AreaMethod.my_field_tac]
simp_1 [in AreaMethod.my_field_tac]
simp_frac_12 [in AreaMethod.my_field_tac]
simp_14 [in AreaMethod.my_field_tac]
simp_frac_3 [in AreaMethod.my_field_tac]
simp_12 [in AreaMethod.my_field_tac]
simp_10 [in AreaMethod.my_field_tac]
simp_frac_11 [in AreaMethod.my_field_tac]
simp_frac_1 [in AreaMethod.my_field_tac]
simp_11 [in AreaMethod.my_field_tac]
simp_8 [in AreaMethod.my_field_tac]
simp_3 [in AreaMethod.my_field_tac]
simp_frac_8 [in AreaMethod.my_field_tac]
simp_frac_13 [in AreaMethod.my_field_tac]
simp_6 [in AreaMethod.my_field_tac]
simp_frac_14 [in AreaMethod.my_field_tac]
simp_15 [in AreaMethod.my_field_tac]
square_1 [in AreaMethod.examples_6]
square_2 [in AreaMethod.examples_6]
square_to_py [in AreaMethod.pythagoras_difference]
symmetric_point_ex [in AreaMethod.basic_geometric_facts]
symmetric_point_unicity [in AreaMethod.pythagoras_difference_lemmas]
S_4 [in AreaMethod.geometry_tools_lemmas]
S_3 [in AreaMethod.geometry_tools_lemmas]
S_1 [in AreaMethod.geometry_tools_lemmas]
S_0 [in AreaMethod.geometry_tools_lemmas]
S_2 [in AreaMethod.geometry_tools_lemmas]
S4Simpl_2 [in AreaMethod.geometry_tools]
S4Simpl_3 [in AreaMethod.geometry_tools]
S4Simpl_6 [in AreaMethod.geometry_tools]
S4Simpl_1 [in AreaMethod.geometry_tools]
S4Simpl_5 [in AreaMethod.geometry_tools]
S4Simpl_4 [in AreaMethod.geometry_tools]
S4_6 [in AreaMethod.geometry_tools_lemmas]
S4_1 [in AreaMethod.geometry_tools_lemmas]
S4_4 [in AreaMethod.geometry_tools_lemmas]
S4_8 [in AreaMethod.geometry_tools_lemmas]
S4_3 [in AreaMethod.geometry_tools_lemmas]
S4_2 [in AreaMethod.geometry_tools_lemmas]
S4_7 [in AreaMethod.geometry_tools_lemmas]
S4_5 [in AreaMethod.geometry_tools_lemmas]


T

test_uniformize_dir_seg_1 [in AreaMethod.geometry_tools]
test_area_on_parallel_1 [in AreaMethod.tests_elimination_tactics_areas]
test_on_parallel_d_1 [in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_foot_2 [in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_1 [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_1 [in AreaMethod.tests_elimination_tactics_py]
test_inter_ll_4 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_d_5 [in AreaMethod.tests_elimination_tactics_py]
test_only_use_area_coordinates_1 [in AreaMethod.free_points_elimination]
test_on_line_d_12 [in AreaMethod.tests_elimination_tactics_ratios]
test_3 [in AreaMethod.elimination_prepare]
test_on_line_d_11 [in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_parallel_3 [in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_1b [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_2 [in AreaMethod.tests_elimination_tactics_py]
test_uniformize_dir_seg_2 [in AreaMethod.geometry_tools]
test_simpl_left_right_3 [in AreaMethod.area_method]
test_inter_ll_gen_3 [in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_line_d_1 [in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_gen_2 [in AreaMethod.tests_elimination_tactics_ratios]
test_inter_ll_1 [in AreaMethod.tests_elimination_tactics_py]
test_area_on_line_d_3 [in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_2b [in AreaMethod.tests_elimination_tactics_ratios]
test_on_line_4 [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_line_d_4 [in AreaMethod.tests_elimination_tactics_py]
test_area_on_inter_parallel_parallel_1 [in AreaMethod.tests_elimination_tactics_areas]
test_uniformize_dir_seg_4 [in AreaMethod.geometry_tools]
test_inter_ll_gen_1 [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_d_4 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_parallel_d_4 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_parallel_d_1 [in AreaMethod.tests_elimination_tactics_py]
test_area_on_parallel_d_3 [in AreaMethod.tests_elimination_tactics_areas]
test_area_on_perp_d_2 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_foot_3 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_5 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_perp_d_1 [in AreaMethod.tests_elimination_tactics_py]
test_area_inter_ll_3 [in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_2 [in AreaMethod.tests_elimination_tactics_ratios]
test_inter_ll_3 [in AreaMethod.tests_elimination_tactics_py]
test_area_on_line_1 [in AreaMethod.tests_elimination_tactics_areas]
test_area_on_perp_d_1 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_line_d_3 [in AreaMethod.tests_elimination_tactics_py]
test_2 [in AreaMethod.elimination_prepare]
test_py_on_parallel_d_2 [in AreaMethod.tests_elimination_tactics_py]
test_1 [in AreaMethod.elimination_prepare]
test_area_on_perp_2 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_line_4_c [in AreaMethod.tests_elimination_tactics_py]
test_uniformize_dir_seg_5 [in AreaMethod.geometry_tools]
test_inter_ll_4 [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_foot_2 [in AreaMethod.tests_elimination_tactics_py]
test_6 [in AreaMethod.elimination_prepare]
test_area_on_parallel_d_2 [in AreaMethod.tests_elimination_tactics_areas]
test_area_on_line_3 [in AreaMethod.tests_elimination_tactics_areas]
test_py_simpl [in AreaMethod.pythagoras_difference]
test_on_foot_1 [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_perp_d_3 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_d_2 [in AreaMethod.tests_elimination_tactics_py]
test_area_on_line_d_2 [in AreaMethod.tests_elimination_tactics_areas]
test_area_on_parallel_2 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_foot_1 [in AreaMethod.tests_elimination_tactics_py]
test_check_ratio_hyp [in AreaMethod.area_method]
test_area_on_perp_1 [in AreaMethod.tests_elimination_tactics_areas]
test_inter_ll_3 [in AreaMethod.tests_elimination_tactics_ratios]
test_area_inter_ll_2 [in AreaMethod.tests_elimination_tactics_areas]
test_on_foot_2 [in AreaMethod.tests_elimination_tactics_ratios]
test_elim [in AreaMethod.examples_6]
test_py_on_line_d_1 [in AreaMethod.tests_elimination_tactics_py]
test_area_inter_ll_1 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_perp_4 [in AreaMethod.tests_elimination_tactics_py]
test_only_use_area_coordinates_3 [in AreaMethod.free_points_elimination]
test_py_on_line_3 [in AreaMethod.tests_elimination_tactics_py]
test_inter_ll [in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_foot_1 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_foot_5 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_perp_d_2 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_4_b [in AreaMethod.tests_elimination_tactics_py]
test_uniformize_dir_seg_3 [in AreaMethod.geometry_tools]
test_inter_ll_4b [in AreaMethod.tests_elimination_tactics_ratios]
test_area_on_inter_line_parallel_1 [in AreaMethod.tests_elimination_tactics_areas]
test_py_on_parallel_d_3 [in AreaMethod.tests_elimination_tactics_py]
test_simpl_left_right_2 [in AreaMethod.area_method]
test_py_on_line_4 [in AreaMethod.tests_elimination_tactics_py]
test_only_use_area_coordinates_2 [in AreaMethod.free_points_elimination]
test_inter_ll_3b [in AreaMethod.tests_elimination_tactics_ratios]
test_py_on_line_d_6 [in AreaMethod.tests_elimination_tactics_py]
test_uniformize_pys [in AreaMethod.pythagoras_difference]
test_py_on_foot_4 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_line_1 [in AreaMethod.tests_elimination_tactics_py]
test_4 [in AreaMethod.elimination_prepare]
test_inter_ll_5 [in AreaMethod.tests_elimination_tactics_ratios]
test_inter_ll_2 [in AreaMethod.tests_elimination_tactics_py]
test_py_on_perp_3 [in AreaMethod.tests_elimination_tactics_py]
test_simpl_left_right_1 [in AreaMethod.area_method]
test_basic_simpl [in AreaMethod.pythagoras_difference]
test_area_on_line_2 [in AreaMethod.tests_elimination_tactics_areas]
test_5 [in AreaMethod.elimination_prepare]
test_py_on_line_2 [in AreaMethod.tests_elimination_tactics_py]
test_area_on_parallel_d_1 [in AreaMethod.tests_elimination_tactics_areas]
test1 [in AreaMethod.bench_normalization_tactics]
test10 [in AreaMethod.bench_normalization_tactics]
test11 [in AreaMethod.bench_normalization_tactics]
test12 [in AreaMethod.bench_normalization_tactics]
test13 [in AreaMethod.bench_normalization_tactics]
test15 [in AreaMethod.bench_normalization_tactics]
test16 [in AreaMethod.bench_normalization_tactics]
test172 [in AreaMethod.bench_normalization_tactics]
test173 [in AreaMethod.bench_normalization_tactics]
test174 [in AreaMethod.bench_normalization_tactics]
test18 [in AreaMethod.bench_normalization_tactics]
test19 [in AreaMethod.bench_normalization_tactics]
test2 [in AreaMethod.bench_normalization_tactics]
test20 [in AreaMethod.bench_normalization_tactics]
test21 [in AreaMethod.bench_normalization_tactics]
test22 [in AreaMethod.bench_normalization_tactics]
test23 [in AreaMethod.bench_normalization_tactics]
test24 [in AreaMethod.bench_normalization_tactics]
test25 [in AreaMethod.bench_normalization_tactics]
test26 [in AreaMethod.bench_normalization_tactics]
test27 [in AreaMethod.bench_normalization_tactics]
test28 [in AreaMethod.bench_normalization_tactics]
test29 [in AreaMethod.bench_normalization_tactics]
test3 [in AreaMethod.bench_normalization_tactics]
test30 [in AreaMethod.bench_normalization_tactics]
test31 [in AreaMethod.bench_normalization_tactics]
test32 [in AreaMethod.bench_normalization_tactics]
test35 [in AreaMethod.bench_normalization_tactics]
test36 [in AreaMethod.bench_normalization_tactics]
test4 [in AreaMethod.bench_normalization_tactics]
test40 [in AreaMethod.bench_normalization_tactics]
test41 [in AreaMethod.bench_normalization_tactics]
test42 [in AreaMethod.bench_normalization_tactics]
test43 [in AreaMethod.bench_normalization_tactics]
test44 [in AreaMethod.bench_normalization_tactics]
test45 [in AreaMethod.bench_normalization_tactics]
test46 [in AreaMethod.bench_normalization_tactics]
test47 [in AreaMethod.bench_normalization_tactics]
test48 [in AreaMethod.bench_normalization_tactics]
test49 [in AreaMethod.bench_normalization_tactics]
test5 [in AreaMethod.bench_normalization_tactics]
test50 [in AreaMethod.bench_normalization_tactics]
test51 [in AreaMethod.bench_normalization_tactics]
test52 [in AreaMethod.bench_normalization_tactics]
test53 [in AreaMethod.bench_normalization_tactics]
test54 [in AreaMethod.bench_normalization_tactics]
test55 [in AreaMethod.bench_normalization_tactics]
test56 [in AreaMethod.bench_normalization_tactics]
test57 [in AreaMethod.bench_normalization_tactics]
test58 [in AreaMethod.bench_normalization_tactics]
test59 [in AreaMethod.bench_normalization_tactics]
test6 [in AreaMethod.bench_normalization_tactics]
test60 [in AreaMethod.bench_normalization_tactics]
test61 [in AreaMethod.bench_normalization_tactics]
test62 [in AreaMethod.bench_normalization_tactics]
test65 [in AreaMethod.bench_normalization_tactics]
test7 [in AreaMethod.bench_normalization_tactics]
test8 [in AreaMethod.bench_normalization_tactics]
test9 [in AreaMethod.bench_normalization_tactics]
thales [in AreaMethod.advanced_parallel_lemmas]
thales_2 [in AreaMethod.advanced_parallel_lemmas]
th2_41 [in AreaMethod.examples_2]
th6_259 [in AreaMethod.examples_6]
th6_41_b [in AreaMethod.examples_3]
th6_257 [in AreaMethod.examples_2]
th6_258 [in AreaMethod.examples_3]
th6_239 [in AreaMethod.examples_3]
th6_256_1 [in AreaMethod.examples_2]
th6_232 [in AreaMethod.examples_3]
th6_43 [in AreaMethod.examples_2]
th6_40_Centroid [in AreaMethod.examples_2]
th6_42 [in AreaMethod.examples_2]
th6_7 [in AreaMethod.examples_2]
th6_234_1 [in AreaMethod.examples_3]
th6_41 [in AreaMethod.examples_3]
th6_6 [in AreaMethod.examples_2]
trivial_col2 [in AreaMethod.geometry_tools_lemmas]
trivial_col1 [in AreaMethod.geometry_tools_lemmas]
trivial_col3 [in AreaMethod.geometry_tools_lemmas]
two_sides_par_eq_parallelogram [in AreaMethod.advanced_parallel_lemmas]


U

uniformize_areas_formula2_correct [in AreaMethod.Rgeometry_tools]
uniformize_areas_correct [in AreaMethod.Rgeometry_tools]
uniformize_areas_formula2_correct_gen [in AreaMethod.Rgeometry_tools]


W

weak_parallelogram_weak_3_parallelogram [in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_3 [in AreaMethod.advanced_parallel_lemmas]
weak_parallelogram_weak_2_parallelogram [in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_4 [in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_2 [in AreaMethod.advanced_parallel_lemmas]
weak_2_parallelogram_weak_3_parallelogram [in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_weak_3_parallelogram_1 [in AreaMethod.advanced_parallel_lemmas]
weak_para_1 [in AreaMethod.advanced_parallel_lemmas]
weak_parallelogram_parallelogram [in AreaMethod.advanced_parallel_lemmas]
weak_3_parallelogram_eq_side [in AreaMethod.pythagoras_difference_lemmas]
weak_3_parallelogram_parallel [in AreaMethod.pythagoras_difference_lemmas]


Z

zeroegal [in AreaMethod.geometry_tools_lemmas]



Notation Index

other

_ + _ (F_scope) [in AreaMethod.field]
_ - _ (F_scope) [in AreaMethod.field]
_ ** _ (F_scope) [in AreaMethod.chou_gao_zhang_axioms]
/ _ (F_scope) [in AreaMethod.field]
1 (F_scope) [in AreaMethod.field]
- _ (F_scope) [in AreaMethod.field]
2 (F_scope) [in AreaMethod.field]
_ * _ (F_scope) [in AreaMethod.field]
_ / _ (F_scope) [in AreaMethod.field]
0 (F_scope) [in AreaMethod.field]



Constructor Index

A

AD [in AreaMethod.Rgeometry_tools]
AFinv [in AreaMethod.Rgeometry_tools]
AFmult [in AreaMethod.Rgeometry_tools]
AFopp [in AreaMethod.Rgeometry_tools]
AFplus [in AreaMethod.Rgeometry_tools]
AFvar [in AreaMethod.Rgeometry_tools]
AF0 [in AreaMethod.Rgeometry_tools]
AF1 [in AreaMethod.Rgeometry_tools]
APvar [in AreaMethod.Rgeometry_tools]
AS [in AreaMethod.Rgeometry_tools]


F

FVar [in AreaMethod.Rgeometry_tools]
f_const [in AreaMethod.Rgeometry_tools]
f_imp2 [in AreaMethod.Rgeometry_tools]
f_neq [in AreaMethod.Rgeometry_tools]
f_imp [in AreaMethod.Rgeometry_tools]
f_eq [in AreaMethod.Rgeometry_tools]


P

PVar [in AreaMethod.Rgeometry_tools]



Inductive Index

A

AF [in AreaMethod.Rgeometry_tools]
AP [in AreaMethod.Rgeometry_tools]
AVars [in AreaMethod.Rgeometry_tools]


F

formula [in AreaMethod.Rgeometry_tools]
formula2 [in AreaMethod.Rgeometry_tools]



Definition Index

A

a_ratio [in AreaMethod.area_coords_constructions]


C

Col [in AreaMethod.chou_gao_zhang_axioms]
co_circle [in AreaMethod.euclidean_constructions]


D

Det3 [in AreaMethod.freepoints]


E

eqF [in AreaMethod.Rgeometry_tools]
eq_distance [in AreaMethod.euclidean_constructions]
eq_angle [in AreaMethod.euclidean_constructions]
eq_product [in AreaMethod.euclidean_constructions]


F

Fdiv [in AreaMethod.field]
Feq [in AreaMethod.field]
Fminus [in AreaMethod.field]


H

harmonic [in AreaMethod.euclidean_constructions]


I

implies [in AreaMethod.Rgeometry_tools]
interp_formula2_to_prop [in AreaMethod.Rgeometry_tools]
interp_AF_to_F [in AreaMethod.Rgeometry_tools]
interp_AP_to_Point [in AreaMethod.Rgeometry_tools]
interp_f [in AreaMethod.Rgeometry_tools]
inter_lc [in AreaMethod.euclidean_constructions]
inter_ll [in AreaMethod.construction_lemmas]
inversion [in AreaMethod.euclidean_constructions]
is_circumcenter [in AreaMethod.area_coords_constructions]
is_circumcenter' [in AreaMethod.area_coords_constructions]
is_Lemoine [in AreaMethod.area_coords_constructions]
is_midpoint [in AreaMethod.construction_lemmas]
is_orthocenter [in AreaMethod.area_coords_constructions]
is_orthocenter' [in AreaMethod.area_coords_constructions]
is_centroid [in AreaMethod.area_coords_constructions]


L

list_assoc_inv [in AreaMethod.Rgeometry_tools]


M

mid_point [in AreaMethod.basic_geometric_facts]
mratio [in AreaMethod.construction_lemmas]
m_ratio [in AreaMethod.euclidean_constructions]


N

nateq [in AreaMethod.Rgeometry_tools]
natle [in AreaMethod.Rgeometry_tools]
neqF [in AreaMethod.Rgeometry_tools]


O

on_inter_parallel_parallel [in AreaMethod.construction_lemmas]
on_perp_d [in AreaMethod.euclidean_constructions]
on_line_d [in AreaMethod.construction_lemmas]
on_inter_line_parallel [in AreaMethod.construction_lemmas]
on_circle [in AreaMethod.euclidean_constructions]
on_parallel_d [in AreaMethod.construction_lemmas]
on_line [in AreaMethod.construction_lemmas]
on_perp [in AreaMethod.euclidean_constructions]
on_parallel [in AreaMethod.construction_lemmas]
on_inter_line_perp [in AreaMethod.euclidean_constructions]
on_foot [in AreaMethod.pythagoras_difference]


P

parallel [in AreaMethod.chou_gao_zhang_axioms]
parallelogram [in AreaMethod.parallel_lemmas]
parallel_s [in AreaMethod.area_method]
per [in AreaMethod.pythagoras_difference]
perp [in AreaMethod.pythagoras_difference]
Py [in AreaMethod.pythagoras_difference]
Py4 [in AreaMethod.pythagoras_difference]


S

simplif [in AreaMethod.Rgeometry_tools]
symmetric_point [in AreaMethod.basic_geometric_facts]
S4 [in AreaMethod.chou_gao_zhang_axioms]


T

tangent [in AreaMethod.euclidean_constructions]


U

uniformize_areas_formula2 [in AreaMethod.Rgeometry_tools]
uniformize_areas [in AreaMethod.Rgeometry_tools]


W

weak_3_parallelogram [in AreaMethod.advanced_parallel_lemmas]
weak_2_parallelogram [in AreaMethod.advanced_parallel_lemmas]
weak_parallelogram [in AreaMethod.advanced_parallel_lemmas]



Axiom Index

A

A1b [in AreaMethod.chou_gao_zhang_axioms]
A2a [in AreaMethod.chou_gao_zhang_axioms]
A2b [in AreaMethod.chou_gao_zhang_axioms]
A3a [in AreaMethod.chou_gao_zhang_axioms]
A3b [in AreaMethod.chou_gao_zhang_axioms]
A4 [in AreaMethod.chou_gao_zhang_axioms]
A5 [in AreaMethod.chou_gao_zhang_axioms]
A6 [in AreaMethod.chou_gao_zhang_axioms]


C

chara_not_2 [in AreaMethod.chou_gao_zhang_axioms]
chasles [in AreaMethod.chou_gao_zhang_axioms]


D

DSeg [in AreaMethod.chou_gao_zhang_axioms]


F

F [in AreaMethod.field]
Finv [in AreaMethod.field]
Finv_l [in AreaMethod.field]
Fmult [in AreaMethod.field]
Fmult_assoc [in AreaMethod.field]
Fmult_sym [in AreaMethod.field]
Fmult_1l [in AreaMethod.field]
Fmult_Fplus_distr [in AreaMethod.field]
Fopp [in AreaMethod.field]
Fplus [in AreaMethod.field]
Fplus_Ol [in AreaMethod.field]
Fplus_assoc [in AreaMethod.field]
Fplus_sym [in AreaMethod.field]
Fplus_Fopp_r [in AreaMethod.field]
F0 [in AreaMethod.field]
F1 [in AreaMethod.field]
F1_neq_F0 [in AreaMethod.field]


O

on_foot_area [in AreaMethod.pythagoras_difference]


P

parallel_side_eq_parallel [in AreaMethod.chou_gao_zhang_axioms]
perp_para_perp [in AreaMethod.pythagoras_difference]
perp_perp_para [in AreaMethod.pythagoras_difference]
Point [in AreaMethod.chou_gao_zhang_axioms]


S

S [in AreaMethod.chou_gao_zhang_axioms]
SomePoint [in AreaMethod.Rgeometry_tools]
SomeValue [in AreaMethod.Rgeometry_tools]



Library Index

A

advanced_parallel_lemmas
area_coords_constructions
area_coords_elimination
area_elimination_lemmas
area_method


B

basic_geometric_facts
bench_normalization_tactics


C

chou_gao_zhang_axioms
constructed_points_elimination
construction_lemmas
construction_lemmas_2
construction_tactics


E

elimination_prepare
euclidean_constructions_2
euclidean_constructions
examples_centroid
examples_interactive
examples_circumcenter
examples_1
examples_2
examples_3
examples_4
examples_5
examples_6


F

field
field_general_properties
field_variable_isolation_tactic
freepoints
free_points_elimination


G

general_tactics
geometry_tools
geometry_tools_lemmas


M

my_field_tac


P

parallel_lemmas
pythagoras_difference
pythagoras_difference_lemmas
py_elimination_lemmas


R

ratios_elimination_lemmas
Rgeometry_tools


S

simplify_constructions


T

tests_elimination_tactics_ratios
tests_elimination_tactics_areas
tests_elimination_tactics_py



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (923 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (751 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (17 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (61 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (36 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (43 entries)

This page has been generated by coqdoc