SintCorner

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

theorem ConwaySoifer.Canonical.sint_corner_simplified {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sint T r s) (hs : s ≤ 1 / 10) (hlong0 : 1 - rayLen (T (sideIndex 1)) (vertex 1) (sideDirection 1 true) < rayLen (T (sideIndex 0)) (vertex 0) (sideDirection 0 false)) (hlong0' : 1 - 2 * s < rayLen (T (sideIndex 0)) (vertex 0) (sideDirection 0 false)) (n : Fin 3) : ((Simplified.witness s n).2, (Simplified.witness s n).1) ∉ (T (cornerIndex 0)).carrier