@book{tarski,
  author = 	 {Wolfram Schwabhäuser and Wanda Szmielew and Alfred Tarski},
  title = 	 {{Metamathematische Methoden in der Geometrie}},
  publisher = 	 {Springer-Verlag},
  year = 	 {1983},
  address = 	 {Berlin}
}

@article{amai-complexplane,
        year={2015},
	author = "Mari{\'c}, Filip and Simi{\'c}, Danijela",
	doi = "10.1007/s10472-014-9436-4",
	issn = "1012-2443",
	journal = "Annals of Mathematics and Artificial Intelligence",
	keywords = "Interactive theorem proving; Complex plane geometry; Möbius transformations; 68T15; 51B10; 97I80",
	number = "3-4",
	pages = "271--308",
	publisher = "Springer International Publishing",
	title = "{Formalizing Complex Plane Geometry}",
	url = "http://dx.doi.org/10.1007/s10472-014-9436-4",
	volume = "74"
}

@book{schwerdtfeger,
  title={{Geometry of Complex Numbers: Circle Geometry, Moebius Transformation, Non-euclidean Geometry}},
  author={Schwerdtfeger, Hans},
  year={1979},
  publisher={Courier Corporation}
}

@mastersthesis{makarios,
 title = {{A Mechanical Verification of the Independence of Tarski's Euclidean Axiom}},
  author = {Makarios, Timothy James McKenzie},
  school = {Victoria University of Wellington},
  year = {2012},
  note = {Master Thesis}
}

@Inbook{lobachevsky1840geometrische,
author="Lobatschewsky, Nicolaus",
title="Geometrische Untersuchungen zur Theorie der Parallellinien",
bookTitle="Gau{\ss} und die Anf{\"a}nge der nicht-euklidischen Geometrie",
year="1985",
publisher="Springer Vienna",
address="Vienna",
pages="159--223",
abstract="In der Geometrie fand ich einige Unvollkom-menheiten, welche ich f{\"u}r den Grund halte, warum diese Missenschaft, so lange sie nicht in die Analysis {\"u}bergeht, bis ietzt keinen Schritt vorw{\"a}rts thun konnte aus demienigen Zustande, in welchem sie uns von Guclid {\"u}berkommen ist. Zu den Unvollkommenheiten rechne ich die Dunkelheit in den ersten Begriffen von den geometrischen Gr{\"o}{\ss}en, in der Art und Meise wie man sich die Ausmessung dieser Gr{\"o}{\ss}en vorstellt, und endlich die wichtige L{\"u}cke in der Theorie der Parallelen, welche auszuf{\"u}llen, alle Anstrengungen der Wathematiker bis ietzt vergeblich waren. Die Bem{\"u}hungen Legnedre's haben zu doeser Theorie nichts hinzugef{\"u}gt, indem er gen{\"o}thigt war, den einzigen strengen Gang zu derlassen, sich auf einen Seitenweg zu wenden, und zu H{\"u}lfss{\"a}tzen seine Zuflucht zu nehmen, welche er sich unbegr{\"u}ndeter Weise bemihet als nothwendige Ariome darzustellen.",
isbn="978-3-7091-9511-6",
doi="10.1007/978-3-7091-9511-6_4",
url="https://doi.org/10.1007/978-3-7091-9511-6_4"
}

@article{coghetto2018klein1,
  title={{Klein-Beltrami Model. Part I}},
  author={Coghetto, Roland},
  journal={Formalized Mathematics},
  volume={26},
  number={1},
  pages={21--32},
  year={2018},
  publisher={Sciendo}
}

@article{coghetto2018klein2,
  title={{Klein-Beltrami Model. Part II}},
  author={Coghetto, Roland},
  journal={Formalized Mathematics},
  volume={26},
  number={1},
  pages={33--48},
  year={2018},
  publisher={Sciendo}
}

 	

@article{afp-complex-geometry,
  author  = {Filip Marić and Danijela Simić},
  title   = {Complex Geometry},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/Complex_Geometry.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

