package coq-high-school-geometry
Geometry in Coq for French high school
Install
Dune Dependency
Authors
Maintainers
Sources
v8.16.tar.gz
sha512=694dfe2a60896a4b044854c612cc54462e92864349f35d7b87b6ab40878260d0400d406b8657ac8fed39ae7b27b58ba3b9c9c12082adbf0313d270abfd494dc5
Description
This Coq library is dedicated to high-shool geometry teaching. The axiomatisation for affine Euclidean space is in a non analytic setting. Includes a proof of Ptolemy's theorem.
Tags
category:Mathematics/Geometry/General keyword:geometry keyword:teaching keyword:high school keyword:Ptolemy's theorem logpath:HighSchoolGeometry date:2023-11-18Published: 18 Nov 2023
On This Page