ยซ Up

geocoq dev 55 m 0 s ๐Ÿ†

Context

# 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"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-geocoq.dev coq.dev
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 8h opam install -y --deps-only coq-geocoq.dev coq.dev
Return code
0
Duration
22 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y coq-geocoq.dev coq.dev
Return code
0
Duration
55 m 0 s

Installation size

Total: 59 M

  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.glob
  • 891 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.vo
  • 878 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.vo
  • 844 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.vo
  • 821 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.vo
  • 766 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.vo
  • 739 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/POF_to_Tarski.glob
  • 718 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.vo
  • 639 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.glob
  • 607 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/POF_to_Tarski.vo
  • 606 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.vo
  • 603 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.vo
  • 590 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.vo
  • 516 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.glob
  • 514 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.vo
  • 514 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/sets.vo
  • 485 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.vo
  • 434 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.vo
  • 430 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.vo
  • 407 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.vo
  • 389 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.glob
  • 386 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.glob
  • 379 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.glob
  • 376 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.vo
  • 364 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.vo
  • 361 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.glob
  • 358 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.vo
  • 353 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.glob
  • 333 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.vo
  • 328 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.vo
  • 323 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.vo
  • 317 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.glob
  • 315 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.vo
  • 302 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.vo
  • 299 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.vo
  • 295 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.glob
  • 289 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.glob
  • 278 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.v
  • 278 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.glob
  • 275 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CongR.vo
  • 268 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.vo
  • 264 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.glob
  • 248 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.glob
  • 236 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.vo
  • 230 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.vo
  • 227 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.vo
  • 227 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.vo
  • 216 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.glob
  • 213 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.vo
  • 205 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.vo
  • 203 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.vo
  • 194 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.glob
  • 193 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.vo
  • 190 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.vo
  • 189 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.vo
  • 187 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.vo
  • 181 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.vo
  • 178 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.glob
  • 176 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.vo
  • 172 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.vo
  • 170 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Definitions.glob
  • 170 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/arity.vo
  • 168 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.glob
  • 167 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.glob
  • 166 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.vo
  • 166 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.vo
  • 162 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.glob
  • 161 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.vo
  • 159 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.glob
  • 156 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.glob
  • 154 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/arity.glob
  • 154 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.glob
  • 152 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.glob
  • 151 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.vo
  • 151 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.vo
  • 150 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.glob
  • 150 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.vo
  • 149 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.glob
  • 149 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.vo
  • 149 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.vo
  • 147 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.glob
  • 147 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.glob
  • 146 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.vo
  • 144 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.vo
  • 142 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.v
  • 141 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.vo
  • 139 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.vo
  • 138 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.vo
  • 138 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.glob
  • 135 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.vo
  • 134 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.vo
  • 134 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.glob
  • 130 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.vo
  • 129 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.vo
  • 126 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.vo
  • 126 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.vo
  • 126 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.glob
  • 122 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.vo
  • 121 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.vo
  • 120 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.vo
  • 117 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.vo
  • 115 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/sets.glob
  • 115 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.vo
  • 114 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.vo
  • 113 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.vo
  • 113 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.vo
  • 113 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.vo
  • 113 K ../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
  • 112 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.glob
  • 112 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/euclidean_axioms.vo
  • 112 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.vo
  • 111 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.vo
  • 109 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.vo
  • 109 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.vo
  • 108 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.glob
  • 107 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.glob
  • 107 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.vo
  • 105 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.vo
  • 105 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.v
  • 104 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.vo
  • 104 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.vo
  • 103 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.glob
  • 102 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.vo
  • 101 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.v
  • 101 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CongR.glob
  • 100 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.vo
  • 99 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.v
  • 99 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.vo
  • 98 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.v
  • 97 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_variant.vo
  • 97 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.vo
  • 97 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.glob
  • 97 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Definitions.vo
  • 96 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.vo
  • 96 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.vo
  • 95 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.vo
  • 94 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.vo
  • 94 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.vo
  • 91 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.v
  • 91 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.vo
  • 90 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.vo
  • 89 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.vo
  • 89 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.vo
  • 89 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.vo
  • 88 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.vo
  • 87 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.vo
  • 86 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.vo
  • 86 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.glob
  • 85 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.vo
  • 84 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.vo
  • 83 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.vo
  • 82 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.vo
  • 82 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.glob
  • 81 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.v
  • 80 K ../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
  • 79 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.vo
  • 79 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.vo
  • 78 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.v
  • 78 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes_cantor_dedekind.vo
  • 76 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.glob
  • 76 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.vo
  • 75 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/euclidean_axioms.glob
  • 75 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.v
  • 75 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.glob
  • 74 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.vo
  • 74 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.vo
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.vo
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.glob
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.vo
  • 72 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/parallel_postulates.glob
  • 72 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.glob
  • 72 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.v
  • 71 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.vo
  • 70 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.vo
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.vo
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.vo
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.glob
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.v
  • 67 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.vo
  • 67 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.vo
  • 67 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.glob
  • 66 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.vo
  • 66 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.v
  • 66 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.vo
  • 66 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.vo
  • 66 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.glob
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.v
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.vo
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.glob
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.vo
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.vo
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.vo
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.glob
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.glob
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.vo
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.vo
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.glob
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.glob
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.glob
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.vo
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.glob
  • 63 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.glob
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.glob
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.glob
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.vo
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.vo
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.vo
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.v
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.glob
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.vo
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.glob
  • 61 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.vo
  • 61 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.vo
  • 61 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.vo
  • 59 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.vo
  • 59 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.glob
  • 58 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.vo
  • 58 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.vo
  • 58 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.vo
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.glob
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.vo
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.v
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.glob
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.vo
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/continuity_axioms.glob
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.vo
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.glob
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.glob
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.vo
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.vo
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.glob
  • 54 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.glob
  • 54 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.vo
  • 54 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.glob
  • 54 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_concy.vo
  • 54 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.v
  • 53 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.vo
  • 53 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/main.vo
  • 52 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.vo
  • 52 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.glob
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.v
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/POF_to_Tarski.v
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.glob
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.glob
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.vo
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.v
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.vo
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.glob
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.glob
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/parallel_postulates.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.glob
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.glob
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.glob
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.glob
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.v
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.v
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.vo
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.glob
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.vo
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.vo
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.glob
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.glob
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.glob
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.v
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.glob
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.vo
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.vo
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.vo
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.glob
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.v
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_cantor.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/continuity_axioms.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.v
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/arity.v
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.glob
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.v
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.glob
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.v
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.glob
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.glob
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.glob
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.glob
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.glob
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.glob
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.vo
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.vo
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.vo
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.vo
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.glob
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/sets.v
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.glob
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_variant.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes_cantor_dedekind.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.v
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.v
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.v
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_variant.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.vo
  • 33 K ../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
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.glob
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CongR.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.glob
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.v
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.glob
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.glob
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.glob
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.glob
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.glob
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.v
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.glob
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.glob
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.glob
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.glob
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.v
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.glob
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.glob
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.glob
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_completeness.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.v
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.glob
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.v
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.v
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/gupta_inspired_variant_axioms.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.vo
  • 22 K ../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
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/gupta_inspired_variant_axioms.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.v
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.v
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.v
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.v
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.glob
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.glob
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_cantor.glob
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.v
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.glob
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.v
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CongR.v
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_concy.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.v
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.v
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.v
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.v
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Definitions.v
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_cong_theory.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.v
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.v
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.v
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.v
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.v
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.v
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.v
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.v
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.v
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.vo
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.vo
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.vo
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.vo
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.vo
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_variant.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.vo
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_variant.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/parallel_postulates.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_variant.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.vo
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/continuity_axioms.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/euclidean_axioms.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes_cantor_dedekind.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.glob
  • 6 K ../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
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/triples.vo
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_concy.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.vo
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_cantor.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.vo
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.v
  • 4 K ../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
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.vo
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_variant.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CongR.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_variant.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CongR.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/finish.vo
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_variant.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/gupta_inspired_variant_axioms.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_completeness.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_cong_theory.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/triples.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/cantor_completeness.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/finish.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_cong_theory.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/main.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Utils/triples.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/main.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/GeoCoq/Tactics/finish.glob

Uninstall ๐Ÿงน

Command
opam remove -y coq-geocoq.dev
Return code
0
Missing removes
none
Wrong removes
none