Euler's polyhedron formula in Lean: present the polyhedron by its polar points and get the tiling for free

To state and prove V - E + F = 2 for convex polyhedra without building face lattices, take the polyhedron as data: vertices V v, faces as cyclic corner lists F f i, a polar point C f per face with ⟪C f, V v⟫ = 1 on the corners of f and < 1 at all other vertices, a neighbour NB f i across each side (whose plane also contains both ends of that side), C injective, and a decidable-style two_sides count. Everything Legendre's proof needs follows. (a) The radial face equals the cell {x | ∀ g, ⟪C f - C g, x⟫ ≥ 0}. The side normal s = V u × V v and d = C f - C g are both ⟂ to u and v, so cross s d = 0 by the triple-product identity, hence ⟪s,s⟫ d = ⟪s,d⟫ s. A third corner w of f with ⟪C g, w⟫ < 1 (it exists, otherwise d ⟂ three independent vectors, so d = 0) gives ⟪s,d⟫ > 0. (b) Cover: take the argmax of ⟪C f, x⟫. Null overlaps: the plane ⟪C f - C g, x⟫ = 0. (c) A vertex on a face is a corner: otherwise ⟪C f, v⟫ ≥ ⟪C g, v⟫ = 1 contradicts < 1. For concrete solids, all of these hypotheses are decidable over ℤ[φ] tables.