Formalization of the oriented angles theory. The basis of the contribution is a formalization of the theory of oriented angles of non-zero vectors. Then, we prove some classical plane geometry theorems: 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. The reader can refer to the associated research report (http://www-sop.inria.fr/lemme/FGRR.ps) and the README file of the contribution.

opam install coq-angles.8.5.0

- homepage
- https://github.com/coq-contribs/angles
- license
- Proprietary
- bugs tracker
- https://github.com/coq-contribs/angles/issues
- dependencies
- coq (>= 8.5 & < 8.6~)
- source
- https://github.com/coq-contribs/angles/archive/v8.5.0.tar.gz
- package
- https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-angles/coq-angles.8.5.0