https://hal.inria.fr/inria-00072226Guilhot, FrédériqueFrédériqueGuilhotLEMME - Software and mathematics - CRISAM - Inria Sophia Antipolis - Méditerranée - Inria - Institut National de Recherche en Informatique et en AutomatiqueProofs with Coq of theorems in plane geometry using oriented anglesHAL CCSD2002COQPCOQGEOMETRYTHEOREMPROOFANGLECIRCLE[INFO.INFO-OH] Computer Science [cs]/Other [cs.OH]Inria, Rapport De Recherche2006-05-23 20:09:452022-02-04 03:16:232006-05-31 14:24:26enReportsapplication/pdf1Formalization of the theory of oriented angles of non zero vectors using Coq is reported. Using this theory, some classical plane geometry theorems are proved, among them : the theorem which gives a necessary and sufficient condition so that four points are cocyclic, the one which shows that the reflected points with respect to the sides of a triangle orthocenter are on its circumscribed circle, the Simson's theorem and the Napoleon's theorem. Elaboration of proofs using Coq that followed the traditional proofs in geometry, and the difficulties encountered are described. Use of the interface Pcoq allows notations close to mathematical ones.