@boarders@mathstodon.xyz oh, I think the Fundamental Theorem of Algebra could be proved in 750 lines of Agda. Some of the lines might be a bit long though.