Poncelet's closure theorem

⚠ WARNING: the main statements in the repo depend on more axioms than the "standard three". It additionally depends on native_decide in the Poncelet/Heavy/ folder. These in principle can be replaced by decide +kernel but I don't think any typical PC can finish those proofs with kernel only.

Status

Main statements

• EuclideanGeometry.poncelet: one circle in another on Euclidean plane.
• TODO: intersecting circles, cotangent circles, and separate circles
• TODO: conics in projective plane