# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.9.1 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml # opam file: opam-version: "2.0" synopsis: "A formalization of foundations of geometry in Coq" description: "This subpackage contains a formalization of Euclid's proofs from Book I of the Elements." maintainer: "Julien Narboux <julien@narboux.fr>" authors: ["Michael Beeson <profbeeson@gmail.com>" "Julien Narboux <narboux@unistra.fr>" "Freek Wiedijk <freek@cs.ru.nl>"] license: "LGPL 3" homepage: "http://geocoq.github.io/GeoCoq/" bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" depends: [ "coq-geocoq-axioms" { = "2.4.0" } ] build: [ ["./configure-elements.sh"] [make "-j%{jobs}%"] ] install: [[make "install"]] tags: [ "keyword:geometry" "keyword:neutral geometry" "keyword:euclidean geometry" "keyword:foundations" "keyword:Euclid" "keyword:Elements" "category:Mathematics/Geometry/General" "date:2018-06-13" ] extra-files : [[ "Make.in" "md5=cac845bd85ad41adeeb32378cf505f1c" ]] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.0.tar.gz" checksum: "md5=4a4ad33b4cad9b815a9b5c6308524c63" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-geocoq-elements.2.4.0 coq.8.9.1
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-geocoq-elements.2.4.0 coq.8.9.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-geocoq-elements.2.4.0 coq.8.9.1
Total: 15 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_planeseparation.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_35.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paste5.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_16.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_24.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_07.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear1.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_32.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crisscross.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_45.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_22.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_04.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_35helper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_linereflectionisometry.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_46.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsmeet.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_10.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angletrichotomy.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Euclid4.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_pointreflectionisometry.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareparallelogram.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/euclid_to_tarski.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_notperp.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_diagonalsbisect.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_17.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementinequality.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_42B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_sameside2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearbetween.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_21.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleaddition.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear4.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareunique.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudeofrighttriangle.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_48.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_30helper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_15.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossbar2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_triangletoparallelogram.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_39.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29C.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleordertransitive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_44.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfairhelper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_34.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_20.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_30B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanadditive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/book1.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_47.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_18.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_37.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5b.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectangleparallelogram.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_38.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_26helper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoffunique.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelbetween.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squaresequal.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_altitudebisectsbase.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_10_12.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06a.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_9_5a.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightangleNC.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_01.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_08.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_legsmallerhypotenuse.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_29B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_tactics.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_09.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_14.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_12.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglestransitive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrectangle.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_midpointunique.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_differenceofparts.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/euclidean_defs.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelPasch.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_36A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearitypreserved.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_40.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthantransitive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equaltorightisright.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_droppedperpendicularunique.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesNC.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglessymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_02.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_paralleldef2A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearright.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_interior5.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_43.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_21helper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_outerconnectivity.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_fiveline.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tarskiparallelflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_subtractequals.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trapezoiddiagonals.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_19.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesidesymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Pasch_outer2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twolines.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_EFreflexive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_7.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28A.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28D.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_28C.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_27B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelcollinear.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ABCequalsCBA.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_twoperpsparallel.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extension.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTtransitive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy1.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_righttogether.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_together.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_8_3.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_erectedperpendicularunique.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelNC.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_25.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_23C.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennesspreserved.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_Playfair.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_13.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplements2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_11.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearparallel.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TGsymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_26B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ondiameter.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_33B.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_tworays.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray3.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidecollinear.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_41.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05b.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTsymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angledistinct.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_crossimpliesopposite.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray4.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear1.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_extensionunique.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_trichotomy2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_06.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NChelper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7a.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_layoff.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglereverse.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCorder.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_betweennotequal.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_partnotequalwhole.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_localextension.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidesymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rightreverse.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_parallelsymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squareflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_05.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_NCdistinct.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthanbetween.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidetransitive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_31short.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesidereflexive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/general_tactics.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samesideflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_samenotopposite.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalangleshelper.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_RTcongruence.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementofright.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinear5.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_collinearorder.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_angleorderrespectscongruence2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGsymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGrotate.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruenceflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rectanglerotate.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalanglesreflexive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_doublereverse.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_rayimpliescollinear.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/proposition_03.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthannotequal.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_PGflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_oppositesideflip.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray5.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TTorder.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_lessthancongruence2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6a.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_6b.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_7b.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_supplementsymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_TCreflexive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_squarerectangle.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray1.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_raystrict.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ray2.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencetransitive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_ETreflexive.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_congruencesymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_3_5b.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_inequalitysymmetric.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/GeoCoq/Elements/OriginalProofs/lemma_equalitysymmetric.v
opam remove -y coq-geocoq-elements.2.4.0