Three Squares Theorem. - Anton Danilkin; Loïc Chevalier (Arch. Formal Proofs, 2023)