@MISC{EUCLID12.MIZ,
  AUTHOR = {Coghetto, Roland},
  TITLE = {Circumcenter, Circumcircle, and Centroid of a Triangle},
  DAY = {30},
  MONTH = {December},
  YEAR = {2015},
  ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
  SECTION1 = {Preliminaries},
  SECTION2 = {Betweenness},
  SECTION3 = {Real Plane},
  SECTION4 = {The Midpoint of a Segment},
  SECTION5 = {Perpendicularity},
  SECTION6 = {The Perpendicular Bisector of a Segment},
  SECTION7 = {The circumcircle of a triangle},
  SECTION8 = {Extended Law of sines},
  SECTION9 = {The centroid of a triangle},
  MSC2010 = {51M04, 3B035},
  KEYWORDS = {Euclidean geometry, perpendicular bisector,
  circumcenter, circumcircle, centroid, extended law of sines},
  SUMMARY = {We introduce, suing the Mizar system \cite{Mizar:2015},
  some basic concepts of Euclidean geometry:
  the half length and the midpoint of a segment,
  the perpendicular bisector of a segment, the medians (the cevians
  that join the vertices of a triangle to the midpoints of the
  opposite sides) of a triangle.
  \par
  We prove the existence and uniqueness of the circumcenter of a
  triangle (the intersection of the three perpendicular bisectors of
  the sides of the triangle). The extended law of sines and
  the formula of the radius of
  the Morley's trisector triangle are formalized \cite{Coxeter:1967}.
   \par
  Using the generalized Ceva's Theorem, we prove the existence and
  uniqueness of the centroid (the common point of the
  medians \cite{hartshorne2000geometry}) of a triangle.}}

@BOOK{Coxeter:1967,
 AUTHOR={Coxeter, H.S.M. and Greitzer, S.L.},
 TITLE={Geometry Revisited},
 PUBLISHER={The Mathematical Association of America (Inc.)},
  PAGES={1--7},
 YEAR=1967}

@book{hartshorne2000geometry,
  title={Geometry: {E}uclid and Beyond},
  author={Hartshorne, Robin},
  year={2000},
  pages={51--53},
  publisher={Springer Science \& Business Media}
}

@inproceedings{Mizar:2015,
  author    = {Bancerek, Grzegorz and
               Byli{\'n}ski, Czes{\l}aw and
               Grabowski, Adam and
               Korni{\l}owicz, Artur and
               Matuszewski, Roman and
               Naumowicz, Adam and
               P\c{a}k, Karol and
               Urban, Josef},
  title     = {Mizar: State-of-the-art and Beyond},
  booktitle = {Intelligent Computer Mathematics -- International Conference,
               {CICM} 2015, Washington, DC, USA, July 13--17, 2015, Proceedings},
  pages     = {261--279},
  year      = {2015},
  crossref  = {DBLP:conf/mkm/2015},
  url       = {http://dx.doi.org/10.1007/978-3-319-20615-8_17},
  doi       = {10.1007/978-3-319-20615-8_17}}
