hippocrates_lunes.toml

id = "hippocrates_lunes"
title = "Hippocrates' theorem on lunes"
test = false
module = "LeanEval.Geometry.HippocratesLunes"
holes = ["hippocrates_lunes"]
submitter = "Kim Morrison"
notes = "For a right triangle, the sum of the areas of the two Hippocrates lunes equals the area of the triangle. Trusted helpers (det2, closedHalfDisk, hypotenuseSemidisk, horizontalLune, verticalLune, rightTriangle, …) are non-holes; the Euclidean squared distance is used explicitly to avoid the ℝ×ℝ sup metric. Mathlib has no lune-area result. Candidate from §166 of the Knill survey."
source = "Hippocrates of Chios (c. 440 BC). Knill, §166."