The Lean proof for de Zolt’s theorem in 3D space, done in the (new) Zₚ system. See zp.pdf for details.