# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev Formal proof management system
dune 3.1.1 Fast, portable, and opinionated build system
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.3 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Julien Narboux <julien@narboux.fr>"
homepage: "http://geocoq.github.io/GeoCoq/"
bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
authors: ["Michael Beeson" "Gabriel Braun <gabriel.braun@unistra.fr>" "Pierre Boutry <pierre.boutry@unistra.fr>" "Charly Gries <charly.gries@etu.unistra.fr>" "Julien Narboux <narboux@unistra.fr"]
license: "LGPL 3"
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/GeoCoq"]
depends: [
"ocaml"
"coq" {>= "8.6.2"}
"coq-mathcomp-field" {>= "1.6.4"}
]
synopsis: "A formalization of foundations of geometry in Coq"
flags: light-uninstall
url {
src: "git+https://github.com/GeoCoq/GeoCoq.git"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-geocoq.dev coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 8h opam install -y --deps-only coq-geocoq.dev coq.devopam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y coq-geocoq.dev coq.devTotal: 59 M
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/POF_to_Tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/POF_to_Tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/sets.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CongR.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Definitions.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/arity.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/arity.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/sets.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/euclidean_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CongR.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_variant.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Definitions.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes_cantor_dedekind.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/euclidean_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/parallel_postulates.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/continuity_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_concy.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/main.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/POF_to_Tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/parallel_postulates.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_cantor.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/continuity_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/arity.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/sets.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_variant.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes_cantor_dedekind.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_variant.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CongR.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_completeness.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/gupta_inspired_variant_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/gupta_inspired_variant_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_cantor.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CongR.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_concy.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Definitions.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_cong_theory.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_variant.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_variant.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/parallel_postulates.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_variant.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/continuity_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/euclidean_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes_cantor_dedekind.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/triples.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_concy.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_cantor.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_variant.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CongR.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_variant.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CongR.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/finish.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_variant.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/gupta_inspired_variant_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_completeness.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_cong_theory.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/triples.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_completeness.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/finish.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_cong_theory.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/main.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/triples.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/main.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/finish.globopam remove -y coq-geocoq.dev